let D be set ; :: thesis: for Y being FinSequenceSet of D
for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)
let Y be FinSequenceSet of D; :: thesis: for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)
let F1, F2 be FinSequence of Y; :: thesis: Length (F1 ^ F2) = (Length F1) ^ (Length F2)
B1: ( dom (Length (F1 ^ F2)) = dom (F1 ^ F2) & dom (Length F1) = dom F1 & dom (Length F2) = dom F2 ) by Def1;
then A1: ( len (Length (F1 ^ F2)) = len (F1 ^ F2) & len (Length F1) = len F1 & len (Length F2) = len F2 ) by FINSEQ_3:29;
B2: len ((Length F1) ^ (Length F2)) = (len (Length F1)) + (len (Length F2)) by FINSEQ_1:22;
then A2: len (Length (F1 ^ F2)) = len ((Length F1) ^ (Length F2)) by A1, FINSEQ_1:22;

now :: thesis: for k being Nat st 1 <= k & k <= len (Length (F1 ^ F2)) holds
(Length (F1 ^ F2)) . k = ((Length F1) ^ (Length F2)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (Length (F1 ^ F2)) implies (Length (F1 ^ F2)) . b₁ = ((Length F1) ^ (Length F2)) . b₁ )
assume A3: ( 1 <= k & k <= len (Length (F1 ^ F2)) ) ; :: thesis: (Length (F1 ^ F2)) . b₁ = ((Length F1) ^ (Length F2)) . b₁
then k in dom (Length (F1 ^ F2)) by FINSEQ_3:25;
then A4: (Length (F1 ^ F2)) . k = len ((F1 ^ F2) . k) by Def1;

per cases ( k <= len (Length F1) or len (Length F1) < k ) ;

suppose B5: k <= len (Length F1) ; :: thesis: (Length (F1 ^ F2)) . b₁ = ((Length F1) ^ (Length F2)) . b₁

then A5: ( k in dom F1 & k in dom (Length F1) ) by B1, A3, FINSEQ_3:25;
then ((Length F1) ^ (Length F2)) . k = (Length F1) . k by FINSEQ_1:def 7
.= len (F1 . k) by B5, Def1, B1, A3, FINSEQ_3:25 ;
hence (Length (F1 ^ F2)) . k = ((Length F1) ^ (Length F2)) . k by A5, A4, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A7: len (Length F1) < k ; :: thesis: (Length (F1 ^ F2)) . b₁ = ((Length F1) ^ (Length F2)) . b₁

then (len (Length F1)) + 1 <= k by NAT_1:13;
then k - ((len (Length F1)) + 1) is Nat by NAT_1:21;
then reconsider k1 = (k - (len (Length F1))) - 1 as Nat ;
k <= (len (Length F1)) + (len (Length F2)) by A3, A1, FINSEQ_1:22;
then k - (len (Length F1)) <= len (Length F2) by XREAL_1:20;
then A10: k1 + 1 in dom (Length F2) by FINSEQ_3:25, NAT_1:11;
((Length F1) ^ (Length F2)) . k = (Length F2) . (k1 + 1) by A2, A3, A7, FINSEQ_1:24
.= len (F2 . (k1 + 1)) by A10, Def1 ;
hence (Length (F1 ^ F2)) . k = ((Length F1) ^ (Length F2)) . k by A4, A3, A1, A7, FINSEQ_1:24; :: thesis: verum

end;

end;

end;

hence Length (F1 ^ F2) = (Length F1) ^ (Length F2) by B2, A1, FINSEQ_1:22; :: thesis: verum