let k, t, i, m, n 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 12;

i in dom (M1 ^ M2) by A1, A2, FINSEQ_1:28;

hence Line ((M1 ^ M2),i) = (M1 ^ M2) . i by MATRIX_0:60

.= M2 . n1 by A1, A2, FINSEQ_1:def 7

.= Line (M2,n) by A1, MATRIX_0:60 ;

:: thesis: verum

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 12;

i in dom (M1 ^ M2) by A1, A2, FINSEQ_1:28;

hence Line ((M1 ^ M2),i) = (M1 ^ M2) . i by MATRIX_0:60

.= M2 . n1 by A1, A2, FINSEQ_1:def 7

.= Line (M2,n) by A1, MATRIX_0:60 ;

:: thesis: verum