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 )

( ( 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 ) )

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

end;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 ) )
;

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

end;proof

hence
( a = I_el Y & b = I_el Y )
by A2, BVFUNC_1:def 11; :: thesis: verum
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;(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