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