:: deftheorem Def2 defines divs SURREALI:def 2 :
for lamb, x being object
for X being set
for Inv being Function
for b₅ being set holds
( b₅ = divs (lamb,x,X,Inv) iff for o being object holds
( o in b₅ iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) );