let n, k, m, i 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 i in dom M1 holds
Line (M1 ^ M2),i = Line M1,i
let D be non empty set ; :: thesis: for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st i in dom M1 holds
Line (M1 ^ M2),i = Line M1,i
let M1 be Matrix of n,k,D; :: thesis: for M2 being Matrix of m,k,D st i in dom M1 holds
Line (M1 ^ M2),i = Line M1,i
let M2 be Matrix of m,k,D; :: thesis: ( i in dom M1 implies Line (M1 ^ M2),i = Line M1,i )
assume A1: i in dom M1 ; :: thesis: Line (M1 ^ M2),i = Line M1,i
reconsider i1 = i as Element of NAT by ORDINAL1:def 13;
dom M1 c= dom (M1 ^ M2) by FINSEQ_1:39;
hence Line (M1 ^ M2),i = (M1 ^ M2) . i by A1, MATRIX_2:18
.= M1 . i1 by A1, FINSEQ_1:def 7
.= Line M1,i by A1, MATRIX_2:18 ;
:: thesis: verum