let A, B be Sequence; :: thesis: Card (A ^ B) = (Card A) ^ (Card B)
A1: dom (Card (A ^ B)) = dom (A ^ B) by CARD_3:def 2
.= (dom A) +^ (dom B) by ORDINAL4:def 1
.= (dom (Card A)) +^ (dom B) by CARD_3:def 2
.= (dom (Card A)) +^ (dom (Card B)) by CARD_3:def 2
.= dom ((Card A) ^ (Card B)) by ORDINAL4:def 1 ;
now :: thesis: for x being object st x in dom (Card (A ^ B)) holds
(Card (A ^ B)) . x = ((Card A) ^ (Card B)) . x
let x be object ; :: thesis: ( x in dom (Card (A ^ B)) implies (Card (A ^ B)) . b1 = ((Card A) ^ (Card B)) . b1 )
assume x in dom (Card (A ^ B)) ; :: thesis: (Card (A ^ B)) . b1 = ((Card A) ^ (Card B)) . b1
then A2: x in dom (A ^ B) by CARD_3:def 2;
then reconsider C = x as Ordinal ;
x in (dom A) +^ (dom B) by A2, ORDINAL4:def 1;
per cases then ( C in dom A or ex D being Ordinal st
( D in dom B & C = (dom A) +^ D ) ) by ORDINAL3:38;
suppose A3: C in dom A ; :: thesis: (Card (A ^ B)) . b1 = ((Card A) ^ (Card B)) . b1
then A4: C in dom (Card A) by CARD_3:def 2;
thus (Card (A ^ B)) . x = card ((A ^ B) . x) by A2, CARD_3:def 2
.= card (A . x) by A3, ORDINAL4:def 1
.= (Card A) . x by A3, CARD_3:def 2
.= ((Card A) ^ (Card B)) . x by A4, ORDINAL4:def 1 ; :: thesis: verum
end;
suppose ex D being Ordinal st
( D in dom B & C = (dom A) +^ D ) ; :: thesis: (Card (A ^ B)) . b1 = ((Card A) ^ (Card B)) . b1
then consider D being Ordinal such that
A5: ( D in dom B & C = (dom A) +^ D ) ;
A6: ( D in dom (Card B) & C = (dom (Card A)) +^ D ) by A5, CARD_3:def 2;
thus (Card (A ^ B)) . x = card ((A ^ B) . x) by A2, CARD_3:def 2
.= card (B . D) by A5, ORDINAL4:def 1
.= (Card B) . D by A5, CARD_3:def 2
.= ((Card A) ^ (Card B)) . x by A6, ORDINAL4:def 1 ; :: thesis: verum
end;
end;
end;
hence Card (A ^ B) = (Card A) ^ (Card B) by A1, FUNCT_1:2; :: thesis: verum