let F, G be FinSequence; :: thesis: Card (F ^ G) = (Card F) ^ (Card G)
A1: dom (Card F) = dom F by CARD_3:def 2;
A2: dom (Card G) = dom G by CARD_3:def 2;
A3: len (Card F) = len F by A1, FINSEQ_3:31;
A4: len (Card G) = len G by A2, FINSEQ_3:31;
A5: dom ((Card F) ^ (Card G)) = Seg ((len (Card F)) + (len (Card G))) by FINSEQ_1:def 7
.= dom (F ^ G) by A3, A4, FINSEQ_1:def 7 ;

now

let x be set ; :: thesis: ( x in dom (F ^ G) implies ((Card F) ^ (Card G)) . b₁ = card ((F ^ G) . b₁) )
assume A6: x in dom (F ^ G) ; :: thesis: ((Card F) ^ (Card G)) . b₁ = card ((F ^ G) . b₁)
then A7: x in Seg ((len F) + (len G)) by FINSEQ_1:def 7;
reconsider k = x as Element of NAT by A6;
A8: ( 1 <= k & k <= (len F) + (len G) ) by A7, FINSEQ_1:3;

per cases ( k <= len F or len F < k ) ;

suppose k <= len F ; :: thesis: ((Card F) ^ (Card G)) . b₁ = card ((F ^ G) . b₁)

then A9: k in dom F by A8, FINSEQ_3:27;
hence ((Card F) ^ (Card G)) . x = (Card F) . k by A1, FINSEQ_1:def 7
.= card (F . k) by A9, CARD_3:def 2
.= card ((F ^ G) . x) by A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose len F < k ; :: thesis: ((Card F) ^ (Card G)) . b₁ = card ((F ^ G) . b₁)

then not k in dom F by FINSEQ_3:27;
then consider n being Nat such that
A10: ( n in dom G & k = (len F) + n ) by A6, FINSEQ_1:38;
thus ((Card F) ^ (Card G)) . x = (Card G) . n by A2, A3, A10, FINSEQ_1:def 7
.= card (G . n) by A10, CARD_3:def 2
.= card ((F ^ G) . x) by A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence Card (F ^ G) = (Card F) ^ (Card G) by A5, CARD_3:def 2; :: thesis: verum