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 )
assume A2: a 'eqv' b = I_el Y ; :: thesis: a = b
A3: 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 A2, Def14;
hence (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE ; :: thesis: verum

end;

A4: 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 )
A5: (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE by A3;
( (a . x) '&' ('not' (b . x)) = TRUE or (a . x) '&' ('not' (b . x)) = FALSE ) by XBOOLEAN:def 3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) by A5; :: thesis: verum

end;

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

proof

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

end;

consider k3 being Function such that
A9: ( a = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A10: ( b = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A6, A9, A10;
hence a = b by A9, A10, 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 )
assume A11: a = b ; :: thesis: a 'eqv' b = I_el Y
A12: 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 A11, XBOOLEAN:def 3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) ; :: thesis: verum

end;

A13: 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 A12;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A12;
then (a 'eqv' b) . x = TRUE by Def12;
hence (a 'eqv' b) . x = (I_el Y) . x by Def14; :: thesis: verum

end;

consider k3 being Function such that
A14: ( a 'eqv' b = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A15: ( I_el Y = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A13, A14, A15;
hence a 'eqv' b = I_el Y by A14, A15, FUNCT_1:9; :: thesis: verum

end;

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