let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a 'eqv' b = I_el Y iff a = b )
A1: for a, b being Element of Funcs Y,BOOLEAN st a 'eqv' b = I_el Y holds
a = b

proof

let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a 'eqv' b = I_el Y implies a = b )
consider k3 being Function such that
A2: a = k3 and
A3: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A4: b = k4 and
A5: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
assume A6: a 'eqv' b = I_el Y ; :: thesis: a = b
A7: for x being Element of Y holds (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE

proof

let x be Element of Y; :: thesis: (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE
(a 'eqv' b) . x = 'not' ((a . x) 'xor' (b . x)) by Def12;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A6, Def14;
hence (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE ; :: thesis: verum

end;

A8: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )

proof

let x be Element of Y; :: thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
A9: ( (a . x) '&' ('not' (b . x)) = TRUE or (a . x) '&' ('not' (b . x)) = FALSE ) by XBOOLEAN:def 3;
(('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE by A7;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) by A9; :: thesis: verum

end;

for x being Element of Y holds a . x = b . x

proof

let x be Element of Y; :: thesis: a . x = b . x
('not' (a . x)) '&' (b . x) = FALSE by A8;
then A10: ( ( 'not' (a . x) = TRUE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = TRUE ) ) by MARGREL1:45, XBOOLEAN:def 3;
(a . x) '&' ('not' (b . x)) = FALSE by A8;
hence a . x = b . x by A10; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A2, A4;
hence a = b by A2, A3, A4, A5, FUNCT_1:9; :: thesis: verum

end;

for a, b being Element of Funcs Y,BOOLEAN st a = b holds
a 'eqv' b = I_el Y

proof

let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a = b implies a 'eqv' b = I_el Y )
consider k3 being Function such that
A11: a 'eqv' b = k3 and
A12: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A13: I_el Y = k4 and
A14: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
assume A15: a = b ; :: thesis: a 'eqv' b = I_el Y
A16: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )

proof

let x be Element of Y; :: thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
( b . x = TRUE iff 'not' (b . x) = FALSE ) ;
then ( ( a . x = FALSE & 'not' (b . x) = TRUE ) or ( a . x = TRUE & 'not' (b . x) = FALSE ) ) by A15, XBOOLEAN:def 3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) ; :: thesis: verum

end;

for x being Element of Y holds (a 'eqv' b) . x = (I_el Y) . x

proof

let x be Element of Y; :: thesis: (a 'eqv' b) . x = (I_el Y) . x
(a . x) '&' ('not' (b . x)) = FALSE by A16;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A16;
then (a 'eqv' b) . x = TRUE by Def12;
hence (a 'eqv' b) . x = (I_el Y) . x by Def14; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A11, A13;
hence a 'eqv' b = I_el Y by A11, A12, A13, A14, FUNCT_1:9; :: thesis: verum

end;

hence ( a 'eqv' b = I_el Y iff a = b ) by A1; :: thesis: verum