let D be non empty set ; :: thesis: for F1, F2 being FinSequence_of_Matrix of D holds Width (F1 ^ F2) = (Width F1) ^ (Width F2)
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: Width (F1 ^ F2) = (Width F1) ^ (Width F2)
set F12 = F1 ^ F2;
A1: len (F1 ^ F2) = (len F1) + (len F2) by FINSEQ_1:22;
len F2 = len (Width F2) by CARD_1:def 7;
then A2: dom (Width F2) = dom F2 by FINSEQ_3:29;
A3: len ((Width F1) ^ (Width F2)) = (len F1) + (len F2) by CARD_1:def 7;
A4: len (Width (F1 ^ F2)) = len (F1 ^ F2) by CARD_1:def 7;
then A5: dom ((Width F1) ^ (Width F2)) = dom (Width (F1 ^ F2)) by A1, A3, FINSEQ_3:29;
A6: len F1 = len (Width F1) by CARD_1:def 7;
then A7: dom (Width F1) = dom F1 by FINSEQ_3:29;

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

let k be Nat; :: thesis: ( 1 <= k & k <= (len F1) + (len F2) implies (Width (F1 ^ F2)) . k = ((Width F1) ^ (Width F2)) . k )
assume that
A8: 1 <= k and
A9: k <= (len F1) + (len F2) ; :: thesis: (Width (F1 ^ F2)) . k = ((Width F1) ^ (Width F2)) . k
A10: k in dom ((Width F1) ^ (Width F2)) by A3, A8, A9, FINSEQ_3:25;

now :: thesis: ((Width F1) ^ (Width F2)) . k = (Width (F1 ^ F2)) . k

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

suppose A11: k in dom (Width F1) ; :: thesis: ((Width F1) ^ (Width F2)) . k = (Width (F1 ^ F2)) . k

hence ((Width F1) ^ (Width F2)) . k = (Width F1) . k by FINSEQ_1:def 7
.= width (F1 . k) by A11, Def4
.= width ((F1 ^ F2) . k) by A7, A11, FINSEQ_1:def 7
.= (Width (F1 ^ F2)) . k by A5, A10, Def4 ;
:: thesis: verum

end;

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

then consider n being Nat such that
A12: n in dom (Width F2) and
A13: k = (len F1) + n by A6;
thus ((Width F1) ^ (Width F2)) . k = (Width F2) . n by A6, A12, A13, FINSEQ_1:def 7
.= width (F2 . n) by A12, Def4
.= width ((F1 ^ F2) . k) by A2, A12, A13, FINSEQ_1:def 7
.= (Width (F1 ^ F2)) . k by A5, A10, Def4 ; :: thesis: verum

end;

end;

end;

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

end;

hence Width (F1 ^ F2) = (Width F1) ^ (Width F2) by A4, A1, A3; :: thesis: verum