let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a
let a be Function of Y,BOOLEAN; :: thesis: a 'eqv' (I_el Y) = a
let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: K11((a 'eqv' (I_el Y)),x) = K11(a,x)
(a 'eqv' (I_el Y)) . x = ((a 'imp' (I_el Y)) '&' ((I_el Y) 'imp' a)) . x by BVFUNC_4:7
.= ((('not' a) 'or' (I_el Y)) '&' ((I_el Y) 'imp' a)) . x by BVFUNC_4:8
.= ((('not' a) 'or' (I_el Y)) '&' (('not' (I_el Y)) 'or' a)) . x by BVFUNC_4:8
.= ((I_el Y) '&' (('not' (I_el Y)) 'or' a)) . x by BVFUNC_1:10
.= ((I_el Y) '&' ((O_el Y) 'or' a)) . x by BVFUNC_1:2
.= ((I_el Y) '&' a) . x by BVFUNC_1:9
.= a . x by BVFUNC_1:6 ;
hence K11((a 'eqv' (I_el Y)),x) = K11(a,x) ; :: thesis: verum