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 ;
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 ;
hence (Line (A,i)) ^ (Line (B,i)) = (A ^^ B) . i by
.= Line ((A ^^ B),i) by ;
:: thesis: verum