let A, B be with_cardinal_domain Sequence; :: thesis: ( dom A in dom B implies A ^ B is with_cardinal_domain )
assume A1: dom A in dom B ; :: thesis: A ^ B is with_cardinal_domain
A2: dom (A ^ B) = (dom A) +^ (dom B) by ORDINAL4:def 1;

per cases ( dom B is infinite or dom B is finite ) ;

suppose dom B is infinite ; :: thesis: A ^ B is with_cardinal_domain

hence A ^ B is with_cardinal_domain by A1, A2, ThAdd; :: thesis: verum

end;

suppose A3: dom B is finite ; :: thesis: A ^ B is with_cardinal_domain

dom A c= dom B by A1, ORDINAL1:def 2;
hence A ^ B is with_cardinal_domain by A2, A3; :: thesis: verum

end;

end;