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 ) ;
per cases then ( n = 0 or n = 1 or n = 2 or n > 2 ) ;
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;
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;
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;
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;
end;