let N, n be Nat; :: thesis: for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
let seq1, seq2 be Real_Sequence of N; :: thesis: (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom (seq1 + seq2) = NAT by FUNCT_2:def 1;
thus (seq1 + seq2) . n = (seq1 + seq2) /. m
.= (seq1 /. m) + (seq2 /. m) by A1, VFUNCT_1:def 1
.= (seq1 . n) + (seq2 . n) ; :: thesis: verum