let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis:
let D be set ; :: thesis:
let M be Matrix of D; :: thesis:
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:
let n be Nat; :: thesis:
assume A3: n in dom (f1 ^ f2) ; :: thesis:

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:
take j ; :: thesis:
thus [i,j] in Indices M by A5; :: thesis:
thus (f1 ^ f2) /. n = M * (i,j) by A4, A6, FINSEQ_4:68; :: thesis:

end;

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:
take j ; :: thesis:
thus [i,j] in Indices M by A9; :: thesis:
thus (f1 ^ f2) /. n = M * (i,j) by A7, A8, A10, FINSEQ_4:69; :: thesis:

end;