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

dom M1 c= dom (M1 ^ M2) by FINSEQ_1:26;

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

.= M1 . i1 by A1, FINSEQ_1:def 7

.= Line (M1,i) by A1, MATRIX_0:60 ;

:: thesis: verum

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

dom M1 c= dom (M1 ^ M2) by FINSEQ_1:26;

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

.= M1 . i1 by A1, FINSEQ_1:def 7

.= Line (M1,i) by A1, MATRIX_0:60 ;

:: thesis: verum