reconsider FR = F_Real as non trivial well-unital doubleLoopStr ;
reconsider X = x as Function of O,FR ;
set S = SgmX ((RelIncl O),(support b));
consider y being FinSequence of the carrier of FR such that
A1: ( len y = len (SgmX ((RelIncl O),(support b))) & eval (b,X) = Product y ) and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power FR) . (((X * (SgmX ((RelIncl O),(support b)))) /. i),((b * (SgmX ((RelIncl O),(support b)))) /. i)) by POLYNOM2:def 2;
reconsider Y = y as FinSequence of the carrier of F_Real ;
A3: dom y = dom (SgmX ((RelIncl O),(support b))) by A1, FINSEQ_3:29;
defpred S₁[ Nat] means ( O <= len y implies Product (Y | O) is integer );
A4: S₁[ 0 ]

proof

Y | 0 = <*> the carrier of F_Real ;
then Product (Y | 0) = 1_ F_Real by GROUP_4:8;
hence S₁[ 0 ] ; :: thesis: verum

end;

A5: Y | (len y) = Y by FINSEQ_1:58;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A8: n + 1 <= len y ; :: thesis: Product (Y | (n + 1)) is integer
then A9: n + 1 in dom y by FINSEQ_3:25, NAT_1:11;
then A10: Y . (n + 1) = Y /. (n + 1) by PARTFUN1:def 6;
Y | (n + 1) = (Y | n) ^ <*(Y . (n + 1))*> by A8, NAT_1:13, FINSEQ_5:83;
then A11: Product (Y | (n + 1)) = (Product (Y | n)) * (Y /. (n + 1)) by A10, GROUP_4:6;
reconsider A = x * (SgmX ((RelIncl O),(support b))) as INT -valued FinSequence of the carrier of F_Real ;
set I = A /. (n + 1);
RelIncl O linearly_orders support b by PRE_POLY:82;
then A12: rng (SgmX ((RelIncl O),(support b))) = support b by PRE_POLY:def 2;
dom X = O by FUNCT_2:def 1;
then dom (X * (SgmX ((RelIncl O),(support b)))) = dom (SgmX ((RelIncl O),(support b))) by A12, RELAT_1:27;
then A13: ( (X * (SgmX ((RelIncl O),(support b)))) /. (n + 1) = (X * (SgmX ((RelIncl O),(support b)))) . (n + 1) & (X * (SgmX ((RelIncl O),(support b)))) . (n + 1) = A /. (n + 1) ) by A3, A9, PARTFUN1:def 6;
then A14: y /. (n + 1) = (power F_Real) . ((A /. (n + 1)),((b * (SgmX ((RelIncl O),(support b)))) /. (n + 1))) by A8, NAT_1:11, A2;
reconsider I = A /. (n + 1) as Element of F_Real by A13;
defpred S₂[ Nat] means (power F_Real) . (I,O) is integer ;
(power F_Real) . (I,0) = 1_ F_Real by GROUP_1:def 7;
then A15: S₂[ 0 ] ;
A16: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
(power F_Real) . (I,(k + 1)) = ((power F_Real) . (I,k)) * I by GROUP_1:def 7;
hence ( S₂[k] implies S₂[k + 1] ) ; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A15, A16);
then y /. (n + 1) is integer by A14;
hence Product (Y | (n + 1)) is integer by A11, A8, NAT_1:13, A7; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A6);
hence eval (b,x) is integer by A5, A1; :: thesis: verum