let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for a, b, c, d being Element of L holds <%a,b%> *' <%c,d%> = <%(a * c),((a * d) + (b * c)),(b * d)%>

let a, b, c, d be Element of L; :: thesis: <%a,b%> *' <%c,d%> = <%(a * c),((a * d) + (b * c)),(b * d)%>

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

A1: <%c,d%> . 0 = c by POLYNOM5:38;

A2: <%c,d%> . 1 = d by POLYNOM5:38;

( not not n = 0 & ... & not n = 2 or n > 2 ) ;

let a, b, c, d be Element of L; :: thesis: <%a,b%> *' <%c,d%> = <%(a * c),((a * d) + (b * c)),(b * d)%>

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

A1: <%c,d%> . 0 = c by POLYNOM5:38;

A2: <%c,d%> . 1 = d by POLYNOM5:38;

( not not n = 0 & ... & not n = 2 or n > 2 ) ;

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

end;

suppose A3:
n = 0
; :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

hence (<%a,b%> *' <%c,d%>) . n =
a * (<%c,d%> . 0)
by UPROOTS:37

.= <%(a * c),((a * d) + (b * c)),(b * d)%> . n by A1, A3, NIVEN:23 ;

:: thesis: verum

end;.= <%(a * c),((a * d) + (b * c)),(b * d)%> . n by A1, A3, NIVEN:23 ;

:: thesis: verum

suppose A4:
n = 1
; :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

hence (<%a,b%> *' <%c,d%>) . n =
(a * (<%c,d%> . (0 + 1))) + (b * (<%c,d%> . 0))
by UPROOTS:37

.= <%(a * c),((a * d) + (b * c)),(b * d)%> . n by A1, A2, A4, NIVEN:24 ;

:: thesis: verum

end;.= <%(a * c),((a * d) + (b * c)),(b * d)%> . n by A1, A2, A4, NIVEN:24 ;

:: thesis: verum

suppose A5:
n = 2
; :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

<%c,d%> . 2 = 0. L
by POLYNOM5:38;

hence <%(a * c),((a * d) + (b * c)),(b * d)%> . n = (a * (<%c,d%> . (1 + 1))) + (b * (<%c,d%> . 1)) by A2, A5, NIVEN:25

.= (<%a,b%> *' <%c,d%>) . n by A5, UPROOTS:37 ;

:: thesis: verum

end;hence <%(a * c),((a * d) + (b * c)),(b * d)%> . n = (a * (<%c,d%> . (1 + 1))) + (b * (<%c,d%> . 1)) by A2, A5, NIVEN:25

.= (<%a,b%> *' <%c,d%>) . n by A5, UPROOTS:37 ;

:: thesis: verum

suppose A6:
n > 2
; :: thesis: (<%a,b%> *' <%c,d%>) . n = <%(a * c),((a * d) + (b * c)),(b * d)%> . n

then A7:
n >= 2 + 1
by NAT_1:13;

consider k being Nat such that

A8: n = k + 1 by A6, NAT_1:6;

A9: len <%c,d%> <= 2 by POLYNOM5:39;

(k + 1) - 1 >= 3 - 1 by A6, A8, NAT_1:13;

then ( <%c,d%> . (k + 1) = 0. L & <%c,d%> . k = 0. L ) by A6, A8, A9, XXREAL_0:2, ALGSEQ_1:8;

hence <%(a * c),((a * d) + (b * c)),(b * d)%> . n = (a * (<%c,d%> . (k + 1))) + (b * (<%c,d%> . k)) by A7, NIVEN:26

.= (<%a,b%> *' <%c,d%>) . n by A8, UPROOTS:37 ;

:: thesis: verum

end;consider k being Nat such that

A8: n = k + 1 by A6, NAT_1:6;

A9: len <%c,d%> <= 2 by POLYNOM5:39;

(k + 1) - 1 >= 3 - 1 by A6, A8, NAT_1:13;

then ( <%c,d%> . (k + 1) = 0. L & <%c,d%> . k = 0. L ) by A6, A8, A9, XXREAL_0:2, ALGSEQ_1:8;

hence <%(a * c),((a * d) + (b * c)),(b * d)%> . n = (a * (<%c,d%> . (k + 1))) + (b * (<%c,d%> . k)) by A7, NIVEN:26

.= (<%a,b%> *' <%c,d%>) . n by A8, UPROOTS:37 ;

:: thesis: verum