let k, m, n be Nat; :: thesis: for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
(M1 ^ M2) @ = (M1 @) ^^ (M2 @)
let D be non empty set ; :: thesis: for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
(M1 ^ M2) @ = (M1 @) ^^ (M2 @)
let M1 be Matrix of n,k,D; :: thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds
(M1 ^ M2) @ = (M1 @) ^^ (M2 @)
let M2 be Matrix of m,k,D; :: thesis: ( width M1 = width M2 implies (M1 ^ M2) @ = (M1 @) ^^ (M2 @) )
assume A1: width M1 = width M2 ; :: thesis: (M1 ^ M2) @ = (M1 @) ^^ (M2 @)
A2: Seg (len ((M1 @) ^^ (M2 @))) = dom ((M1 @) ^^ (M2 @)) by FINSEQ_1:def 3
.= (dom (M1 @)) /\ (dom (M2 @)) by PRE_POLY:def 4
.= (dom (M1 @)) /\ (Seg (len (M2 @))) by FINSEQ_1:def 3
.= (Seg (len (M1 @))) /\ (Seg (len (M2 @))) by FINSEQ_1:def 3
.= (Seg (width M1)) /\ (Seg (len (M2 @))) by MATRIX_0:def 6
.= (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_0:def 6
.= Seg (width M1) by A1 ;
A3: dom ((M1 ^ M2) @) = Seg (len ((M1 ^ M2) @)) by FINSEQ_1:def 3;
A4: len ((M1 ^ M2) @) = width (M1 ^ M2) by MATRIX_0:def 6
.= width M1 by A1, Th24
.= len ((M1 @) ^^ (M2 @)) by A2, FINSEQ_1:6 ;

now :: thesis: for i being Nat st i in dom ((M1 ^ M2) @) holds
((M1 ^ M2) @) . i = ((M1 @) ^^ (M2 @)) . i

let i be Nat; :: thesis: ( i in dom ((M1 ^ M2) @) implies ((M1 ^ M2) @) . i = ((M1 @) ^^ (M2 @)) . i )
assume A5: i in dom ((M1 ^ M2) @) ; :: thesis: ((M1 ^ M2) @) . i = ((M1 @) ^^ (M2 @)) . i
then A6: i in Seg (width (M1 ^ M2)) by A3, MATRIX_0:def 6;
A7: i in dom ((M1 @) ^^ (M2 @)) by A4, A3, A5, FINSEQ_1:def 3;
then A8: i in (dom (M1 @)) /\ (dom (M2 @)) by PRE_POLY:def 4;
then A9: i in dom (M2 @) by XBOOLE_0:def 4;
A10: i in dom (M1 @) by A8, XBOOLE_0:def 4;
reconsider m1 = (M1 @) . i, m2 = (M2 @) . i as FinSequence ;
i in (Seg (len (M1 @))) /\ (dom (M2 @)) by A8, FINSEQ_1:def 3;
then i in (Seg (len (M1 @))) /\ (Seg (len (M2 @))) by FINSEQ_1:def 3;
then i in (Seg (width M1)) /\ (Seg (len (M2 @))) by MATRIX_0:def 6;
then A11: i in (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_0:def 6;
thus ((M1 ^ M2) @) . i = Line (((M1 ^ M2) @),i) by A5, MATRIX_0:60
.= Col ((M1 ^ M2),i) by A6, MATRIX_0:59
.= (Col (M1,i)) ^ (Col (M2,i)) by A1, A11, Th26
.= (Line ((M1 @),i)) ^ (Col (M2,i)) by A1, A11, MATRIX_0:59
.= (Line ((M1 @),i)) ^ (Line ((M2 @),i)) by A1, A11, MATRIX_0:59
.= (Line ((M1 @),i)) ^ m2 by A9, MATRIX_0:60
.= m1 ^ m2 by A10, MATRIX_0:60
.= ((M1 @) ^^ (M2 @)) . i by A7, PRE_POLY:def 4 ; :: thesis: verum

end;

hence (M1 ^ M2) @ = (M1 @) ^^ (M2 @) by A4, FINSEQ_2:9; :: thesis: verum