let n be Nat; :: thesis: for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )
let x be Surreal; :: thesis: for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )
let Inv be Function; :: thesis: ( Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued implies ( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered ) )
assume A1: Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued ; :: thesis: ( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )
defpred S₁[ Nat] means ( (divL (x,Inv)) . $1 is surreal-membered & (divR (x,Inv)) . $1 is surreal-membered );
{} is surreal-membered ;
then A2: S₁[ 0 ] by Th1;
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
( (L_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} & (R_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} ) by XBOOLE_1:7, XBOOLE_1:33;
then A5: ( Inv is (L_ x) \ {0_No} -surreal-valued & Inv is (R_ x) \ {0_No} -surreal-valued ) by A1;
( divset (((divL (x,Inv)) . m),x,((L_ x) \ {0_No}),Inv) is surreal-membered & divset (((divL (x,Inv)) . m),x,((R_ x) \ {0_No}),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,((L_ x) \ {0_No}),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,((R_ x) \ {0_No}),Inv) is surreal-membered ) by A5, Th5, A4;
then A6: ( divset (((divL (x,Inv)) . m),x,(L_ x),Inv) is surreal-membered & divset (((divL (x,Inv)) . m),x,(R_ x),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,(L_ x),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,(R_ x),Inv) is surreal-membered ) by Th8;
( (divL (x,Inv)) . (m + 1) = (((divL (x,Inv)) . m) \/ (divset (((divL (x,Inv)) . m),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . m),x,(L_ x),Inv)) & (divR (x,Inv)) . (m + 1) = (((divR (x,Inv)) . m) \/ (divset (((divL (x,Inv)) . m),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . m),x,(R_ x),Inv)) ) by Th6;
hence S₁[m + 1] by A4, A6; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A3);
hence ( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered ) ; :: thesis: verum