let f1, f2 be FinSequence of (TOP-REAL 2); 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 ; 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; ( ( 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) )
; 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; ( 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)
; 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;
suppose A4:
n in dom f1
;
ex i, j being Nat st
( [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
;
ex j being Nat st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )take
j
;
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )thus
[i,j] in Indices M
by A5;
(f1 ^ f2) /. n = M * (i,j)thus
(f1 ^ f2) /. n = M * (
i,
j)
by A4, A6, FINSEQ_4:68;
verum end; suppose
ex
m being
Nat st
(
m in dom f2 &
n = (len f1) + m )
;
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
;
ex j being Nat st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )take
j
;
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )thus
[i,j] in Indices M
by A9;
(f1 ^ f2) /. n = M * (i,j)thus
(f1 ^ f2) /. n = M * (
i,
j)
by A7, A8, A10, FINSEQ_4:69;
verum end; end;