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

now :: thesis: ( a '&' b = I_el Y implies ( a = I_el Y & b = I_el Y ) )

assume A1: a '&' b = I_el Y ; :: thesis: ( a = I_el Y & b = I_el Y )

per cases ( ( a = I_el Y & b = I_el Y ) or ( a = I_el Y & b <> I_el Y ) or ( a <> I_el Y & b = I_el Y ) or ( a <> I_el Y & b <> I_el Y ) ) ;

suppose ( a = I_el Y & b = I_el Y ) ; :: thesis: ( a = I_el Y & b = I_el Y )

hence ( a = I_el Y & b = I_el Y ) ; :: thesis: verum

end;

suppose ( a = I_el Y & b <> I_el Y ) ; :: thesis: ( a = I_el Y & b = I_el Y )

hence ( a = I_el Y & b = I_el Y ) by A1, BVFUNC_1:6; :: thesis: verum

end;

suppose ( a <> I_el Y & b = I_el Y ) ; :: thesis: ( a = I_el Y & b = I_el Y )

hence ( a = I_el Y & b = I_el Y ) by A1, BVFUNC_1:6; :: thesis: verum

end;

suppose A2: ( a <> I_el Y & b <> I_el Y ) ; :: thesis: ( a = I_el Y & b = I_el Y )

for x being Element of Y holds a . x = TRUE

proof

let x be Element of Y; :: thesis: a . x = TRUE
(a '&' b) . x = TRUE by A1, BVFUNC_1:def 11;
then (a . x) '&' (b . x) = TRUE by MARGREL1:def 20;
hence a . x = TRUE by MARGREL1:12; :: thesis: verum

end;

hence ( a = I_el Y & b = I_el Y ) by A2, BVFUNC_1:def 11; :: thesis: verum

end;

end;

end;

hence ( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y ) ; :: thesis: verum