let N be Element of NAT ; :: thesis: for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1
let seq1, seq2 be Real_Sequence of N; :: thesis: seq1 + seq2 = seq2 + seq1
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (seq1 + seq2) . n = (seq2 + seq1) . n
thus (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) by Th4
.= (seq2 + seq1) . n by Th4 ; :: thesis: verum