let F be Field; for X1, X2 being finite Subset of F
for x being Element of F st not x in X1 & not x in X2 & X1 misses X2 holds
(LagBPoly (X1,x)) *' (LagBPoly (X2,x)) = LagBPoly ((X1 \/ X2),x)
let X1, X2 be finite Subset of F; for x being Element of F st not x in X1 & not x in X2 & X1 misses X2 holds
(LagBPoly (X1,x)) *' (LagBPoly (X2,x)) = LagBPoly ((X1 \/ X2),x)
let x be Element of F; ( not x in X1 & not x in X2 & X1 misses X2 implies (LagBPoly (X1,x)) *' (LagBPoly (X2,x)) = LagBPoly ((X1 \/ X2),x) )
assume A1:
( not x in X1 & not x in X2 & X1 misses X2 )
; (LagBPoly (X1,x)) *' (LagBPoly (X2,x)) = LagBPoly ((X1 \/ X2),x)
A2:
( rng (canFS X1) = X1 & rng (canFS X2) = X2 )
by FUNCT_2:def 3;
then reconsider z1 = canFS X1, z2 = canFS X2 as one-to-one FinSequence of the carrier of F by FINSEQ_1:def 4;
reconsider z12 = z1 ^ z2 as one-to-one FinSequence of the carrier of F by A1, A2, FINSEQ_3:91;
A3:
rng z12 = X1 \/ X2
by A2, FINSEQ_1:31;
set rP1 = rpoly (((len z1) |-> 1),z1);
set rP2 = rpoly (((len z2) |-> 1),z2);
set rP12 = rpoly (((len z12) |-> 1),z12);
Roots (~ (Product (rpoly (((len z1) |-> 1),z1)))) = rng z1
by Th53;
then
not x is_a_root_of ~ (Product (rpoly (((len z1) |-> 1),z1)))
by A1, A2, POLYNOM5:def 10;
then A4:
eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x) <> 0. F
by POLYNOM5:def 7;
Roots (~ (Product (rpoly (((len z2) |-> 1),z2)))) = rng z2
by Th53;
then
not x is_a_root_of ~ (Product (rpoly (((len z2) |-> 1),z2)))
by A1, A2, POLYNOM5:def 10;
then
eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x) <> 0. F
by POLYNOM5:def 7;
then A5: ((eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x)) ") * ((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ") =
((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) * (eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x))) "
by A4, VECTSP_2:11
.=
(eval (((~ (Product (rpoly (((len z1) |-> 1),z1)))) *' (~ (Product (rpoly (((len z2) |-> 1),z2))))),x)) "
by POLYNOM4:24
;
A6: ((len z1) |-> 1) ^ ((len z2) |-> 1) =
((len z1) + (len z2)) |-> 1
by FINSEQ_2:123
.=
(len z12) |-> 1
by FINSEQ_1:22
;
( len ((len z1) |-> 1) = len z1 & len ((len z2) |-> 1) = len z2 )
;
then
rpoly (((len (z1 ^ z2)) |-> 1),z12) = (rpoly (((len z1) |-> 1),z1)) ^ (rpoly (((len z2) |-> 1),z2))
by A6, Th43;
then A7: ~ (Product (rpoly (((len z12) |-> 1),z12))) =
~ ((Product (rpoly (((len z1) |-> 1),z1))) * (Product (rpoly (((len z2) |-> 1),z2))))
by GROUP_4:5
.=
(~ (Product (rpoly (((len z1) |-> 1),z1)))) *' (~ (Product (rpoly (((len z2) |-> 1),z2))))
by POLYNOM3:def 10
;
LagBPoly (X2,x) = ((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ") * (~ (Product (rpoly (((len z2) |-> 1),z2))))
by A2, Def2;
hence (LagBPoly (X1,x)) *' (LagBPoly (X2,x)) =
(((eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x)) ") * (~ (Product (rpoly (((len z1) |-> 1),z1))))) *' (((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ") * (~ (Product (rpoly (((len z2) |-> 1),z2)))))
by A2, Def2
.=
((eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x)) ") * ((~ (Product (rpoly (((len z1) |-> 1),z1)))) *' (((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ") * (~ (Product (rpoly (((len z2) |-> 1),z2))))))
by POLYALG1:10
.=
((eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x)) ") * (((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ") * ((~ (Product (rpoly (((len z2) |-> 1),z2)))) *' (~ (Product (rpoly (((len z1) |-> 1),z1))))))
by POLYALG1:10
.=
(((eval ((~ (Product (rpoly (((len z1) |-> 1),z1)))),x)) ") * ((eval ((~ (Product (rpoly (((len z2) |-> 1),z2)))),x)) ")) * ((~ (Product (rpoly (((len z2) |-> 1),z2)))) *' (~ (Product (rpoly (((len z1) |-> 1),z1)))))
by POLYALG1:8
.=
LagBPoly ((X1 \/ X2),x)
by A5, A3, A7, Def2
;
verum