let L be non empty right_zeroed addLoopStr ; 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; <%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 ; FUNCT_2:def 8 (<%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
;
(<%z0,z1,z2%> + <%z3,z4,z5%>) . n = <%(z0 + z3),(z1 + z4),(z2 + z5)%> . nthen
(
<%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;
verum end; suppose
n = 1
;
(<%z0,z1,z2%> + <%z3,z4,z5%>) . n = <%(z0 + z3),(z1 + z4),(z2 + z5)%> . nthen
(
<%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;
verum end; suppose
n = 2
;
(<%z0,z1,z2%> + <%z3,z4,z5%>) . n = <%(z0 + z3),(z1 + z4),(z2 + z5)%> . nthen
(
<%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;
verum end; suppose
n > 2
;
(<%z0,z1,z2%> + <%z3,z4,z5%>) . n = <%(z0 + z3),(z1 + z4),(z2 + z5)%> . nthen
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;
verum end;