let K be Field; :: thesis: for G1, G2 being FinSequence_of_Matrix of K holds
( Len (G1 (+) G2) = Len G1 & Width (G1 (+) G2) = Width G1 )
let G1, G2 be FinSequence_of_Matrix of K; :: thesis: ( Len (G1 (+) G2) = Len G1 & Width (G1 (+) G2) = Width G1 )
set G12 = G1 (+) G2;
A1: ( dom (Len G1) = dom G1 & dom (Len (G1 (+) G2)) = dom (G1 (+) G2) & dom (Width G1) = dom G1 & dom (Width (G1 (+) G2)) = dom (G1 (+) G2) & dom (G1 (+) G2) = dom G1 ) by Def10, Def3, Def4;

now

let i be Nat; :: thesis: ( i in dom (Len (G1 (+) G2)) implies (Len (G1 (+) G2)) . i = (Len G1) . i )
assume A2: i in dom (Len (G1 (+) G2)) ; :: thesis: (Len (G1 (+) G2)) . i = (Len G1) . i
thus (Len (G1 (+) G2)) . i = len ((G1 (+) G2) . i) by A2, Def3
.= len ((G1 . i) + (G2 . i)) by A1, A2, Def10
.= len (G1 . i) by MATRIX_3:def 3
.= (Len G1) . i by A1, A2, Def3 ; :: thesis: verum

end;

hence Len (G1 (+) G2) = Len G1 by A1, FINSEQ_1:17; :: thesis: Width (G1 (+) G2) = Width G1

now

let i be Nat; :: thesis: ( i in dom (Width (G1 (+) G2)) implies (Width (G1 (+) G2)) . i = (Width G1) . i )
assume A3: i in dom (Width (G1 (+) G2)) ; :: thesis: (Width (G1 (+) G2)) . i = (Width G1) . i
thus (Width (G1 (+) G2)) . i = width ((G1 (+) G2) . i) by A3, Def4
.= width ((G1 . i) + (G2 . i)) by A1, A3, Def10
.= width (G1 . i) by MATRIX_3:def 3
.= (Width G1) . i by A1, A3, Def4 ; :: thesis: verum

end;

hence Width (G1 (+) G2) = Width G1 by A1, FINSEQ_1:17; :: thesis: verum