for A, B being with_cardinal_domain Sequence st dom A in dom B holds
A ^ B is with_cardinal_domain