let t, k, m, n, i be Nat; :: thesis: for D being non empty set
for M1 being Matrix of t,k,D
for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds
Line (M1 ^ M2),i = Line M2,n
let D be non empty set ; :: thesis: for M1 being Matrix of t,k,D
for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds
Line (M1 ^ M2),i = Line M2,n
let M1 be Matrix of t,k,D; :: thesis: for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds
Line (M1 ^ M2),i = Line M2,n
let M2 be Matrix of m,k,D; :: thesis: ( n in dom M2 & i = (len M1) + n implies Line (M1 ^ M2),i = Line M2,n )
assume that
A1: n in dom M2 and
A2: i = (len M1) + n ; :: thesis: Line (M1 ^ M2),i = Line M2,n
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
i in dom (M1 ^ M2) by A1, A2, FINSEQ_1:41;
hence Line (M1 ^ M2),i = (M1 ^ M2) . i by MATRIX_2:18
.= M2 . n1 by A1, A2, FINSEQ_1:def 7
.= Line M2,n by A1, MATRIX_2:18 ;
:: thesis: verum