let f1 be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: for f2 being without+infty Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )
let f2 be without+infty Function of [:NAT,NAT:],ExtREAL; :: thesis: for n, m being Nat holds
( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )
let n, m be Nat; :: thesis: ( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )
A1: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
then reconsider z = [n,m] as Element of [:NAT,NAT:] by ZFMISC_1:87;
[n,m] in [:NAT,NAT:] by A1, ZFMISC_1:87;
hence ( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) ) by Th7; :: thesis: verum