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 ;

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

hence
(M1 ^ M2) @ = (M1 @) ^^ (M2 @)
by A4, FINSEQ_2:9; :: thesis: verum((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;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