let F, G be FinSequence; :: thesis: Card (F ^ G) = (Card F) ^ (Card G)
A1: dom (Card G) = dom G by CARD_3:def 2;
then A2: len (Card G) = len G by FINSEQ_3:29;
A3: dom (Card F) = dom F by CARD_3:def 2;
then A4: len (Card F) = len F by FINSEQ_3:29;

A5: now :: thesis: for x being object st x in dom (F ^ G) holds
((Card F) ^ (Card G)) . x = card ((F ^ G) . x)

let x be object ; :: 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 reconsider k = x as Element of NAT ;
x in Seg ((len F) + (len G)) by A6, FINSEQ_1:def 7;
then A7: 1 <= k by FINSEQ_1:1;

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

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

then A8: k in dom F by A7, FINSEQ_3:25;
hence ((Card F) ^ (Card G)) . x = (Card F) . k by A3, FINSEQ_1:def 7
.= card (F . k) by A8, CARD_3:def 2
.= card ((F ^ G) . x) by A8, 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:25;
then consider n being Nat such that
A9: n in dom G and
A10: k = (len F) + n by A6, FINSEQ_1:25;
thus ((Card F) ^ (Card G)) . x = (Card G) . n by A1, A4, A9, A10, FINSEQ_1:def 7
.= card (G . n) by A9, CARD_3:def 2
.= card ((F ^ G) . x) by A9, A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

dom ((Card F) ^ (Card G)) = Seg ((len (Card F)) + (len (Card G))) by FINSEQ_1:def 7
.= dom (F ^ G) by A4, A2, FINSEQ_1:def 7 ;
hence Card (F ^ G) = (Card F) ^ (Card G) by A5, CARD_3:def 2; :: thesis: verum