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;