let L be non empty right_zeroed addLoopStr ; :: thesis: for z0, z1 being Element of L holds <%z0%> + <%z1%> = <%(z0 + z1)%>
let z0, z1 be Element of L; :: thesis: <%z0%> + <%z1%> = <%(z0 + z1)%>
set p = <%z0%>;
set q = <%z1%>;
set r = <%(z0 + z1)%>;
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (<%z0%> + <%z1%>) . n = <%(z0 + z1)%> . n

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (<%z0%> + <%z1%>) . n = <%(z0 + z1)%> . n

then ( <%z0%> . n = z0 & <%z1%> . n = z1 & <%(z0 + z1)%> . n = z0 + z1 ) by POLYNOM5:32;
hence (<%z0%> + <%z1%>) . n = <%(z0 + z1)%> . n by NORMSP_1:def 2; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (<%z0%> + <%z1%>) . n = <%(z0 + z1)%> . n

then n >= 0 + 1 by NAT_1:13;
then A1: ( <%z0%> . n = 0. L & <%z1%> . n = 0. L & <%(z0 + z1)%> . n = 0. L ) by POLYNOM5:32;
(0. L) + (0. L) = 0. L by RLVECT_1:def 4;
hence (<%z0%> + <%z1%>) . n = <%(z0 + z1)%> . n by A1, NORMSP_1:def 2; :: thesis: verum

end;

end;