let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a '&' c) 'eqv' (b '&' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a '&' c) 'eqv' (b '&' d) = I_el Y )
assume ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; :: thesis: (a '&' c) 'eqv' (b '&' d) = I_el Y
then ( a = b & c = d ) by BVFUNC_1:17;
hence (a '&' c) 'eqv' (b '&' d) = I_el Y by BVFUNC_1:17; :: thesis: verum