let Y be non empty set ; :: thesis: for a being constant Element of Funcs Y,BOOLEAN holds a is_dependent_of %O Y
let a be constant Element of Funcs Y,BOOLEAN ; :: thesis: a is_dependent_of %O Y
for F being set st F in %O Y holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2

proof

let F be set ; :: thesis: ( F in %O Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
A1: for x1, x2 being Element of Y holds a . x1 = a . x2

proof

let x1, x2 be Element of Y; :: thesis: a . x1 = a . x2

per cases ( a = O_el Y or a = I_el Y ) by Th24;

suppose A2: a = O_el Y ; :: thesis: a . x1 = a . x2

then a . x1 = FALSE by Def13;
hence a . x1 = a . x2 by A2, Def13; :: thesis: verum

end;

suppose A3: a = I_el Y ; :: thesis: a . x1 = a . x2

then a . x1 = TRUE by Def14;
hence a . x1 = a . x2 by A3, Def14; :: thesis: verum

end;

end;

end;

assume F in %O Y ; :: thesis: for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
hence for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 by A1; :: thesis: verum

end;

hence a is_dependent_of %O Y by Def18; :: thesis: verum