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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;