let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1
let seq1, seq2 be sequence of X; :: thesis: seq1 + seq2 = seq2 + seq1

now

let n be Element of NAT ; :: thesis: (seq1 + seq2) . n = (seq2 + seq1) . n
thus (seq1 + seq2) . n = (seq2 . n) + (seq1 . n) by NORMSP_1:def 5
.= (seq2 + seq1) . n by NORMSP_1:def 5 ; :: thesis: verum

end;

hence seq1 + seq2 = seq2 + seq1 by FUNCT_2:113; :: thesis: verum