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

proof

let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y implies a = b )
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 Def9;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A6, Def11;
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;

let x be Element of Y; :: according to FUNCT_2:def 8 :: 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:12, XBOOLEAN:def 3;
(a . x) '&' ('not' (b . x)) = FALSE by A8;
hence a . x = b . x by A10; :: thesis: verum

end;

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

proof

let a, b be Function of Y,BOOLEAN; :: thesis: ( a = b implies a 'eqv' b = I_el Y )
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;

let x be Element of Y; :: according to FUNCT_2:def 8 :: 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 Def9;
hence (a 'eqv' b) . x = (I_el Y) . x by Def11; :: thesis: verum

end;

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