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 VALUED_1:def 1, a1, 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 VALUED_1:13, a1, ZFMISC_1:87; :: thesis: verum
end;