let f1, 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))
let n, m be Nat; :: thesis: (f1 + f2) . (n,m) = (f1 . (n,m)) + (f2 . (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)) by Th7; :: thesis: verum