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

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

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

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

end;

suppose n = 1 ; :: thesis: (<%z0,z1%> + <%z2,z3%>) . n = <%(z0 + z2),(z1 + z3)%> . n

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

end;

suppose n > 1 ; :: thesis: (<%z0,z1%> + <%z2,z3%>) . n = <%(z0 + z2),(z1 + z3)%> . n

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

end;

end;