let D be non empty set ; :: thesis: for F1, F2 being FinSequence_of_Matrix of D holds Len (F1 ^ F2) = (Len F1) ^ (Len F2)
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: Len (F1 ^ F2) = (Len F1) ^ (Len F2)
set F12 = F1 ^ F2;
A1: ( len (Len (F1 ^ F2)) = len (F1 ^ F2) & len (F1 ^ F2) = (len F1) + (len F2) & len F1 = len (Len F1) & len F2 = len (Len F2) ) by FINSEQ_1:35, FINSEQ_1:def 18;
A2: len ((Len F1) ^ (Len F2)) = (len F1) + (len F2) by FINSEQ_1:def 18;
then A3: ( dom (Len F1) = dom F1 & dom (Len F2) = dom F2 & dom ((Len F1) ^ (Len F2)) = dom (Len (F1 ^ F2)) ) by A1, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( 1 <= k & k <= (len F1) + (len F2) implies (Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k )
assume A4: ( 1 <= k & k <= (len F1) + (len F2) ) ; :: thesis: (Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k
A5: k in dom ((Len F1) ^ (Len F2)) by A2, A4, FINSEQ_3:27;

now

per cases ( k in dom (Len F1) or ex n being Nat st
( n in dom (Len F2) & k = (len (Len F1)) + n ) ) by A5, FINSEQ_1:38;

suppose A6: k in dom (Len F1) ; :: thesis: ((Len F1) ^ (Len F2)) . k = (Len (F1 ^ F2)) . k

hence ((Len F1) ^ (Len F2)) . k = (Len F1) . k by FINSEQ_1:def 7
.= len (F1 . k) by A6, Def3
.= len ((F1 ^ F2) . k) by A3, A6, FINSEQ_1:def 7
.= (Len (F1 ^ F2)) . k by A3, A5, Def3 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Len F2) & k = (len (Len F1)) + n ) ; :: thesis: ((Len F1) ^ (Len F2)) . k = (Len (F1 ^ F2)) . k

then consider n being Nat such that
A7: ( n in dom (Len F2) & k = (len F1) + n ) by A1;
thus ((Len F1) ^ (Len F2)) . k = (Len F2) . n by A1, A7, FINSEQ_1:def 7
.= len (F2 . n) by A7, Def3
.= len ((F1 ^ F2) . k) by A3, A7, FINSEQ_1:def 7
.= (Len (F1 ^ F2)) . k by A3, A5, Def3 ; :: thesis: verum

end;

end;

end;

hence (Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k ; :: thesis: verum

end;

hence Len (F1 ^ F2) = (Len F1) ^ (Len F2) by A1, A2, FINSEQ_1:18; :: thesis: verum