let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )
thus A1: ( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] ) by FUNCT_2:def 1; :: thesis: ( ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )

hereby :: thesis: for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m))

let n, m be Nat; :: thesis: (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m))
( n in NAT & m in NAT ) by ORDINAL1:def 12;
hence (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) by A1, VALUED_1:def 1, ZFMISC_1:87; :: thesis: verum

end;

hereby :: thesis: verum

let n, m be Nat; :: thesis: (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m))
( n in NAT & m in NAT ) by ORDINAL1:def 12;
hence (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) by A1, VALUED_1:13, ZFMISC_1:87; :: thesis: verum

end;