let L be non empty right_zeroed left_zeroed addLoopStr ; :: thesis: for z0, z1 being Element of L holds <%z0,z1%> = <%z0%> + <%(0. L),z1%>
let z0, z1 be Element of L; :: thesis: <%z0,z1%> = <%z0%> + <%(0. L),z1%>
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n
A1: (<%z0%> + <%(0. L),z1%>) . n = (<%z0%> . n) + (<%(0. L),z1%> . n) by NORMSP_1:def 2;
per cases ( n = 0 or n = 1 or n >= 2 ) by NAT_1:23;
suppose A2: n = 0 ; :: thesis: <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n
then ( <%z0%> . n = z0 & <%(0. L),z1%> . n = 0. L ) by POLYNOM5:32, POLYNOM5:38;
then (<%z0%> + <%(0. L),z1%>) . n = z0 by A1, RLVECT_1:def 4;
hence <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n by A2, POLYNOM5:38; :: thesis: verum
end;
suppose A3: n = 1 ; :: thesis: <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n
then ( <%z0%> . n = 0. L & <%(0. L),z1%> . n = z1 ) by POLYNOM5:32, POLYNOM5:38;
then (<%z0%> + <%(0. L),z1%>) . n = z1 by A1, ALGSTR_1:def 2;
hence <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n by A3, POLYNOM5:38; :: thesis: verum
end;
suppose A4: n >= 2 ; :: thesis: <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n
then ( <%z0%> . n = 0. L & <%(0. L),z1%> . n = 0. L ) by XXREAL_0:2, POLYNOM5:32, POLYNOM5:38;
then (<%z0%> + <%(0. L),z1%>) . n = 0. L by A1, ALGSTR_1:def 2;
hence <%z0,z1%> . n = (<%z0%> + <%(0. L),z1%>) . n by A4, POLYNOM5:38; :: thesis: verum
end;
end;