let n, m, k 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_1:def 3;
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_2:10;
hence (Line A,i) ^ (Line B,i) = (A ^^ B) . i by A2, A1, PRE_POLY:def 4
.= Line (A ^^ B),i by A2, MATRIX_2:10 ;
:: thesis: verum