let Y be non empty set ; for a, b being Element of Funcs Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ('not' b)
let a, b be Element of Funcs Y,BOOLEAN ; 'not' (a 'eqv' b) = a 'eqv' ('not' b)
consider k3 being Function such that
A1:
'not' (a 'eqv' b) = k3
and
A2:
dom k3 = Y
and
rng k3 c= BOOLEAN
by FUNCT_2:def 2;
consider k4 being Function such that
A3:
a 'eqv' ('not' b) = k4
and
A4:
dom k4 = Y
and
rng k4 c= BOOLEAN
by FUNCT_2:def 2;
for x being Element of Y holds ('not' (a 'eqv' b)) . x = (a 'eqv' ('not' b)) . x
then
for u being set st u in Y holds
k3 . u = k4 . u
by A1, A3;
hence
'not' (a 'eqv' b) = a 'eqv' ('not' b)
by A1, A2, A3, A4, FUNCT_1:9; verum