let F be Field; :: thesis: for b1, c1, b2, c2 being Element of F holds <%c1,b1%> *' <%c2,b2%> = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%>
let b1, c1, b2, c2 be Element of F; :: thesis: <%c1,b1%> *' <%c2,b2%> = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%>
set p1 = <%c1,b1%>;
set p2 = <%c2,b2%>;
set q = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%>;
J: 4 -' 1 = 4 - 1 by XREAL_0:def 2;
then K: ( 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3 ) by XREAL_0:def 2;
A: dom (<%c1,b1%> *' <%c2,b2%>) = NAT by FUNCT_2:def 1
.= dom <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> holds
(<%c1,b1%> *' <%c2,b2%>) . o = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . o

let o be object ; :: thesis: ( o in dom <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> implies (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁ )
assume o in dom <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> ; :: thesis: (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁
then reconsider i = o as Element of NAT ;
consider r being FinSequence of the carrier of F such that
B1: ( len r = i + 1 & (<%c1,b1%> *' <%c2,b2%>) . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (<%c1,b1%> . (k -' 1)) * (<%c2,b2%> . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;

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

suppose C: i = 0 ; :: thesis: (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁

then B2: r = <*(r . 1)*> by B1, FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r . 1 = (<%c1,b1%> . (1 -' 1)) * (<%c2,b2%> . ((0 + 1) -' 1)) by C, B1
.= (<%c1,b1%> . (1 -' 1)) * (<%c2,b2%> . 0) by NAT_2:8
.= (<%c1,b1%> . 0) * (<%c2,b2%> . 0) by NAT_2:8
.= c1 * (<%c2,b2%> . 0) by POLYNOM5:38
.= c1 * c2 by POLYNOM5:38 ;
then Sum r = c1 * c2 by B2, RLVECT_1:44;
hence (<%c1,b1%> *' <%c2,b2%>) . o = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . o by B1, C, qua1; :: thesis: verum

end;

suppose C: i = 1 ; :: thesis: (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁

then B3: r = <*(r . 1),(r . 2)*> by B1, FINSEQ_1:44;
B4: dom r = {1,2} by B1, C, FINSEQ_1:def 3, FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r . 1 = (<%c1,b1%> . (1 -' 1)) * (<%c2,b2%> . ((1 + 1) -' 1)) by C, B1
.= (<%c1,b1%> . 0) * (<%c2,b2%> . 1) by K, NAT_2:8
.= c1 * (<%c2,b2%> . 1) by POLYNOM5:38
.= c1 * b2 by POLYNOM5:38 ;
2 in dom r by B4, TARSKI:def 2;
then r . 2 = (<%c1,b1%> . (2 -' 1)) * (<%c2,b2%> . ((1 + 1) -' 2)) by C, B1
.= (<%c1,b1%> . 1) * (<%c2,b2%> . 0) by K, NAT_2:8
.= b1 * (<%c2,b2%> . 0) by POLYNOM5:38
.= b1 * c2 by POLYNOM5:38 ;
then Sum r = (c1 * b2) + (b1 * c2) by B3, B5, RLVECT_1:45
.= (b1 * c2) + (b2 * c1) by GROUP_1:def 12 ;
hence (<%c1,b1%> *' <%c2,b2%>) . o = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . o by B1, C, qua1; :: thesis: verum

end;

suppose C: i = 2 ; :: thesis: (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁

then B3: r = <*(r . 1),(r . 2),(r . 3)*> by B1, FINSEQ_1:45;
B4: dom r = Seg 3 by B1, C, FINSEQ_1:def 3
.= (Seg 2) \/ {(2 + 1)} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2, ENUMSET1:3 ;
then 1 in dom r by ENUMSET1:def 1;
then B5: r . 1 = (<%c1,b1%> . (1 -' 1)) * (<%c2,b2%> . ((2 + 1) -' 1)) by C, B1
.= (<%c1,b1%> . 0) * (<%c2,b2%> . 2) by K, NAT_2:8
.= (<%c1,b1%> . 0) * (0. F) by POLYNOM5:38 ;
2 in dom r by B4, ENUMSET1:def 1;
then B6: r . 2 = (<%c1,b1%> . 1) * (<%c2,b2%> . 1) by K, C, B1
.= b1 * (<%c2,b2%> . 1) by POLYNOM5:38
.= b1 * b2 by POLYNOM5:38 ;
3 in dom r by B4, ENUMSET1:def 1;
then r . 3 = (<%c1,b1%> . 2) * (<%c2,b2%> . ((2 + 1) -' 3)) by K, C, B1
.= (0. F) * (<%c2,b2%> . ((2 + 1) -' 3)) by POLYNOM5:38 ;
then Sum r = ((0. F) + (b1 * b2)) + (0. F) by B3, B5, B6, RLVECT_1:46;
hence (<%c1,b1%> *' <%c2,b2%>) . o = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . o by B1, C, qua1; :: thesis: verum

end;

suppose C: i > 2 ; :: thesis: (<%c1,b1%> *' <%c2,b2%>) . b₁ = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . b₁

D: len <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> <= 3 by qua2;
C1: i >= 2 + 1 by C, NAT_1:13;
then E: <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . i = 0. F by D, XXREAL_0:2, ALGSEQ_1:8;
( len <%c1,b1%> <= 2 & len <%c2,b2%> <= 2 ) by POLYNOM5:39;
then (len <%c1,b1%>) + (len <%c2,b2%>) <= 2 + 2 by XREAL_1:7;
then F: ((len <%c1,b1%>) + (len <%c2,b2%>)) -' 1 <= (2 + 2) -' 1 by lemmonus;
len (<%c1,b1%> *' <%c2,b2%>) <= ((len <%c1,b1%>) + (len <%c2,b2%>)) -' 1 by leng;
then len (<%c1,b1%> *' <%c2,b2%>) <= (2 + 2) -' 1 by F, XXREAL_0:2;
hence (<%c1,b1%> *' <%c2,b2%>) . o = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> . o by J, C1, XXREAL_0:2, E, ALGSEQ_1:8; :: thesis: verum

end;

end;

end;

hence <%c1,b1%> *' <%c2,b2%> = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%> by A; :: thesis: verum