let o be object ; :: thesis: for x being Surreal
for X being set
for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)
let x be Surreal; :: thesis: for X being set
for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)
let X be set ; :: thesis: for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)
let Inv be Function; :: thesis: divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)
thus divs (o,x,X,Inv) c= divs (o,x,(X \ {0_No}),Inv) :: according to XBOOLE_0:def 10 :: thesis: divs (o,x,(X \ {0_No}),Inv) c= divs (o,x,X,Inv)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in divs (o,x,X,Inv) or a in divs (o,x,(X \ {0_No}),Inv) )
assume a in divs (o,x,X,Inv) ; :: thesis: a in divs (o,x,(X \ {0_No}),Inv)
then consider xL being object such that
A1: ( xL in X & xL <> 0_No & a = (1_No +' ((xL +' (-' x)) *' o)) *' (Inv . xL) ) by Def2;
xL in X \ {0_No} by A1, ZFMISC_1:56;
hence a in divs (o,x,(X \ {0_No}),Inv) by A1, Def2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in divs (o,x,(X \ {0_No}),Inv) or a in divs (o,x,X,Inv) )
assume a in divs (o,x,(X \ {0_No}),Inv) ; :: thesis: a in divs (o,x,X,Inv)
then consider xL being object such that
A2: ( xL in X \ {0_No} & xL <> 0_No & a = (1_No +' ((xL +' (-' x)) *' o)) *' (Inv . xL) ) by Def2;
thus a in divs (o,x,X,Inv) by A2, Def2; :: thesis: verum