theorem :: GOBOARD1:23

for f1, f2 being 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) )