let p, q be sequence of L; :: thesis: p + q = q + p

now

let n be Element of NAT ; :: thesis: (p + q) . n = (q + p) . n
thus (p + q) . n = (p . n) + (q . n) by NORMSP_1:def 2
.= (q + p) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence p + q = q + p by FUNCT_2:63; :: thesis: verum