let D1, D2 be set ; :: thesis: ( ( for o being object holds
( o in D1 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ) & ( for o being object holds
( o in D2 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ) implies D1 = D2 )
assume that
A6: for o being object holds
( o in D1 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) and
A7: for o being object holds
( o in D2 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ; :: thesis: D1 = D2

now :: thesis: for o being object holds
( o in D1 iff o in D2 )

let o be object ; :: thesis: ( o in D1 iff o in D2 )
( o in D1 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) by A6;
hence ( o in D1 iff o in D2 ) by A7; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum