let k, m, n be Nat; :: thesis: for D being non empty set

for A being Matrix of n,m,D

for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let D be non empty set ; :: thesis: for A being Matrix of n,m,D

for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let A be Matrix of n,m,D; :: thesis: for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let B be Matrix of n,k,D; :: thesis: for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

set AB = A ^^ B;

A1: ( len (A ^^ B) = n & dom (A ^^ B) = Seg (len (A ^^ B)) ) by FINSEQ_1:def 3, MATRIX_0:def 2;

let i be Nat; :: thesis: ( i in Seg n implies Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i)) )

assume A2: i in Seg n ; :: thesis: Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

( Line (A,i) = A . i & Line (B,i) = B . i ) by A2, MATRIX_0:52;

hence (Line (A,i)) ^ (Line (B,i)) = (A ^^ B) . i by A2, A1, PRE_POLY:def 4

.= Line ((A ^^ B),i) by A2, MATRIX_0:52 ;

:: thesis: verum

for A being Matrix of n,m,D

for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let D be non empty set ; :: thesis: for A being Matrix of n,m,D

for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let A be Matrix of n,m,D; :: thesis: for B being Matrix of n,k,D

for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

let B be Matrix of n,k,D; :: thesis: for i being Nat st i in Seg n holds

Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

set AB = A ^^ B;

A1: ( len (A ^^ B) = n & dom (A ^^ B) = Seg (len (A ^^ B)) ) by FINSEQ_1:def 3, MATRIX_0:def 2;

let i be Nat; :: thesis: ( i in Seg n implies Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i)) )

assume A2: i in Seg n ; :: thesis: Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))

( Line (A,i) = A . i & Line (B,i) = B . i ) by A2, MATRIX_0:52;

hence (Line (A,i)) ^ (Line (B,i)) = (A ^^ B) . i by A2, A1, PRE_POLY:def 4

.= Line ((A ^^ B),i) by A2, MATRIX_0:52 ;

:: thesis: verum