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 (Width (F1 ^ F2)) = len (F1 ^ F2) & len (F1 ^ F2) = (len F1) + (len F2) & len F1 = len (Width F1) & len F2 = len (Width F2) ) by FINSEQ_1:35, FINSEQ_1:def 18;
A2: len ((Width F1) ^ (Width F2)) = (len F1) + (len F2) by FINSEQ_1:def 18;
then A3: ( dom (Width F1) = dom F1 & dom (Width F2) = dom F2 & dom ((Width F1) ^ (Width F2)) = dom (Width (F1 ^ F2)) ) by A1, FINSEQ_3:31;

now

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

now

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

suppose A6: 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 A6, Def4
.= width ((F1 ^ F2) . k) by A3, A6, FINSEQ_1:def 7
.= (Width (F1 ^ F2)) . k by A3, A5, 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
A7: ( n in dom (Width F2) & k = (len F1) + n ) by A1;
thus ((Width F1) ^ (Width F2)) . k = (Width F2) . n by A1, A7, FINSEQ_1:def 7
.= width (F2 . n) by A7, Def4
.= width ((F1 ^ F2) . k) by A3, A7, FINSEQ_1:def 7
.= (Width (F1 ^ F2)) . k by A3, A5, 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 A1, A2, FINSEQ_1:18; :: thesis: verum