let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: for D being set

for M being Matrix of D st ( for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds

for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being 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 Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds

for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

let M be Matrix of D; :: thesis: ( ( for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) implies for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) ) )

assume that

A1: for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) and

A2: for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ; :: thesis: for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

let n be Nat; :: thesis: ( n in dom (f1 ^ f2) implies ex i, j being 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 Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

for M being Matrix of D st ( for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds

for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being 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 Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds

for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

let M be Matrix of D; :: thesis: ( ( for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) implies for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) ) )

assume that

A1: for n being Nat st n in dom f1 holds

ex i, j being Nat st

( [i,j] in Indices M & f1 /. n = M * (i,j) ) and

A2: for n being Nat st n in dom f2 holds

ex i, j being Nat st

( [i,j] in Indices M & f2 /. n = M * (i,j) ) ; :: thesis: for n being Nat st n in dom (f1 ^ f2) holds

ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

let n be Nat; :: thesis: ( n in dom (f1 ^ f2) implies ex i, j being 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 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:25;

end;

( m in dom f2 & n = (len f1) + m ) ) by A3, FINSEQ_1:25;

suppose A4:
n in dom f1
; :: thesis: ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

then consider i, j being Nat such that

A5: [i,j] in Indices M and

A6: f1 /. n = M * (i,j) by A1;

take i ; :: thesis: ex j being 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, A6, FINSEQ_4:68; :: thesis: verum

end;A5: [i,j] in Indices M and

A6: f1 /. n = M * (i,j) by A1;

take i ; :: thesis: ex j being 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, A6, FINSEQ_4:68; :: thesis: verum

suppose
ex m being Nat st

( m in dom f2 & n = (len f1) + m ) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

( m in dom f2 & n = (len f1) + m ) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )

then consider m being Nat such that

A7: m in dom f2 and

A8: n = (len f1) + m ;

consider i, j being Nat such that

A9: [i,j] in Indices M and

A10: f2 /. m = M * (i,j) by A2, A7;

take i ; :: thesis: ex j being 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 A9; :: thesis: (f1 ^ f2) /. n = M * (i,j)

thus (f1 ^ f2) /. n = M * (i,j) by A7, A8, A10, FINSEQ_4:69; :: thesis: verum

end;A7: m in dom f2 and

A8: n = (len f1) + m ;

consider i, j being Nat such that

A9: [i,j] in Indices M and

A10: f2 /. m = M * (i,j) by A2, A7;

take i ; :: thesis: ex j being 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 A9; :: thesis: (f1 ^ f2) /. n = M * (i,j)

thus (f1 ^ f2) /. n = M * (i,j) by A7, A8, A10, FINSEQ_4:69; :: thesis: verum