let n, k, m 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_1:def 7
.= (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_1:def 7
.= 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_1:def 7
.= width M1 by A1, Th28
.= len ((M1 @ ) ^^ (M2 @ )) by A2, FINSEQ_1:8 ;

now

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_1:def 7;
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;
then reconsider m1 = (M1 @ ) . i, m2 = (M2 @ ) . i as FinSequence by A9, PRE_POLY:def 3;
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_1:def 7;
then A11: i in (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_1:def 7;
thus ((M1 ^ M2) @ ) . i = Line ((M1 ^ M2) @ ),i by A5, MATRIX_2:18
.= Col (M1 ^ M2),i by A6, MATRIX_2:17
.= (Col M1,i) ^ (Col M2,i) by A1, A11, Th30
.= (Line (M1 @ ),i) ^ (Col M2,i) by A1, A11, MATRIX_2:17
.= (Line (M1 @ ),i) ^ (Line (M2 @ ),i) by A1, A11, MATRIX_2:17
.= (Line (M1 @ ),i) ^ m2 by A9, MATRIX_2:18
.= m1 ^ m2 by A10, MATRIX_2:18
.= ((M1 @ ) ^^ (M2 @ )) . i by A7, PRE_POLY:def 4 ; :: thesis: verum

end;

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