let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * i,j ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * i,j ) ) holds
for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
let D be set ; :: thesis: for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * i,j ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * i,j ) ) holds
for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
let M be Matrix of D; :: thesis: ( ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * i,j ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * i,j ) ) implies for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j ) )
assume that
A1: for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * i,j ) and
A2: for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * i,j ) ; :: thesis: for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
let n be Element of NAT ; :: thesis: ( n in dom (f1 ^ f2) implies ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j ) )
assume A3: n in dom (f1 ^ f2) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )

per cases ( n in dom f1 or ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ) by A3, FINSEQ_1:38;

suppose A4: n in dom f1 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )

then consider i, j being Element of NAT such that
A5: ( [i,j] in Indices M & f1 /. n = M * i,j ) by A1;
take i ; :: thesis: ex j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
take j ; :: thesis: ( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
thus [i,j] in Indices M by A5; :: thesis: (f1 ^ f2) /. n = M * i,j
thus (f1 ^ f2) /. n = M * i,j by A4, A5, FINSEQ_4:83; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )

then consider m being Nat such that
A6: ( m in dom f2 & n = (len f1) + m ) ;
consider i, j being Element of NAT such that
A7: ( [i,j] in Indices M & f2 /. m = M * i,j ) by A2, A6;
take i ; :: thesis: ex j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
take j ; :: thesis: ( [i,j] in Indices M & (f1 ^ f2) /. n = M * i,j )
thus [i,j] in Indices M by A7; :: thesis: (f1 ^ f2) /. n = M * i,j
thus (f1 ^ f2) /. n = M * i,j by A6, A7, FINSEQ_4:84; :: thesis: verum

end;

end;