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 (F1 ^ F2) = (len F1) + (len F2) by FINSEQ_1:22;
len F2 = len (Len F2) by CARD_1:def 7;
then A2: dom (Len F2) = dom F2 by FINSEQ_3:29;
A3: len ((Len F1) ^ (Len F2)) = (len F1) + (len F2) by CARD_1:def 7;
A4: len (Len (F1 ^ F2)) = len (F1 ^ F2) by CARD_1:def 7;
then A5: dom ((Len F1) ^ (Len F2)) = dom (Len (F1 ^ F2)) by A1, A3, FINSEQ_3:29;
A6: len F1 = len (Len F1) by CARD_1:def 7;
then A7: dom (Len F1) = dom F1 by FINSEQ_3:29;
now :: thesis: for k being Nat st 1 <= k & k <= (len F1) + (len F2) holds
(Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k
let k be Nat; :: thesis: ( 1 <= k & k <= (len F1) + (len F2) implies (Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k )
assume that
A8: 1 <= k and
A9: k <= (len F1) + (len F2) ; :: thesis: (Len (F1 ^ F2)) . k = ((Len F1) ^ (Len F2)) . k
A10: k in dom ((Len F1) ^ (Len F2)) by A3, A8, A9, FINSEQ_3:25;
now :: thesis: ((Len F1) ^ (Len F2)) . k = (Len (F1 ^ F2)) . k
per cases ( k in dom (Len F1) or ex n being Nat st
( n in dom (Len F2) & k = (len (Len F1)) + n ) ) by A10, FINSEQ_1:25;
suppose A11: 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 A11, Def3
.= len ((F1 ^ F2) . k) by A7, A11, FINSEQ_1:def 7
.= (Len (F1 ^ F2)) . k by A5, A10, 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
A12: n in dom (Len F2) and
A13: k = (len F1) + n by A6;
thus ((Len F1) ^ (Len F2)) . k = (Len F2) . n by A6, A12, A13, FINSEQ_1:def 7
.= len (F2 . n) by A12, Def3
.= len ((F1 ^ F2) . k) by A2, A12, A13, FINSEQ_1:def 7
.= (Len (F1 ^ F2)) . k by A5, A10, 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 A4, A1, A3; :: thesis: verum