defpred S₁[ object , object ] means $2 = (1_No +' (($1 +' (-' x)) *' lamb)) *' (Inv . $1);
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z ;
consider D being set such that
A2: for x being object holds
( x in D iff ex y being object st
( y in X \ {0_No} & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take D ; :: thesis: for o being object holds
( o in D iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) )
let o be object ; :: thesis: ( o in D iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) )
thus ( o in D implies ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) :: thesis: ( ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) implies o in D )

proof

assume o in D ; :: thesis: ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) )
then consider y being object such that
A3: ( y in X \ {0_No} & S₁[y,o] ) by A2;
( y in X & y <> 0_No ) by A3, ZFMISC_1:56;
hence ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) by A3; :: thesis: verum

end;

given xL being object such that A4: ( xL in X & xL <> 0_No ) and
A5: o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ; :: thesis: o in D
xL in X \ {0_No} by A4, ZFMISC_1:56;
hence o in D by A2, A5; :: thesis: verum