let D be non empty set ; :: thesis: for G, H, J being Functional_Sequence of D,REAL holds
( G + H = H + G & (G + H) + J = G + (H + J) )
let G, H, J be Functional_Sequence of D,REAL; :: thesis: ( G + H = H + G & (G + H) + J = G + (H + J) )

now :: thesis: for n being Element of NAT holds (G + H) . n = (H + G) . n

let n be Element of NAT ; :: thesis: (G + H) . n = (H + G) . n
thus (G + H) . n = (H . n) + (G . n) by Def5
.= (H + G) . n by Def5 ; :: thesis: verum

end;

hence G + H = H + G by FUNCT_2:63; :: thesis: (G + H) + J = G + (H + J)

now :: thesis: for n being Element of NAT holds ((G + H) + J) . n = (G + (H + J)) . n

let n be Element of NAT ; :: thesis: ((G + H) + J) . n = (G + (H + J)) . n
thus ((G + H) + J) . n = ((G + H) . n) + (J . n) by Def5
.= ((G . n) + (H . n)) + (J . n) by Def5
.= (G . n) + ((H . n) + (J . n)) by RFUNCT_1:8
.= (G . n) + ((H + J) . n) by Def5
.= (G + (H + J)) . n by Def5 ; :: thesis: verum

end;

hence (G + H) + J = G + (H + J) by FUNCT_2:63; :: thesis: verum