let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds a is_dependent_of GPart a
let a be Function of Y,BOOLEAN; :: thesis: a is_dependent_of GPart a
defpred S₁[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S₁[x] } as Subset of Y from DOMAIN_1:sch 7();
defpred S₂[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S₂[x9] } as Subset of Y from DOMAIN_1:sch 7();
for F being set st F in GPart a 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 GPart a implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
assume A1: F in GPart a ; :: thesis: for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
thus for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 :: thesis: verum

proof

let x1, x2 be set ; :: thesis: ( x1 in F & x2 in F implies a . x1 = a . x2 )
assume A2: ( x1 in F & x2 in F ) ; :: thesis: a . x1 = a . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;

now :: thesis: ( ( F = C & a . x1 = a . x2 ) or ( F = D & a . x1 = a . x2 ) )

per cases ( F = C or F = D ) by A1, TARSKI:def 2;

case F = C ; :: thesis: a . x1 = a . x2

then ( ex x being Element of Y st
( x = x1 & a . x = TRUE ) & ex x5 being Element of Y st
( x5 = x2 & a . x5 = TRUE ) ) by A2;
hence a . x1 = a . x2 ; :: thesis: verum

end;

case F = D ; :: thesis: a . x1 = a . x2

then ( ex x being Element of Y st
( x = x1 & a . x = FALSE ) & ex x5 being Element of Y st
( x5 = x2 & a . x5 = FALSE ) ) by A2;
hence a . x1 = a . x2 ; :: thesis: verum

end;

end;

end;

hence a . x1 = a . x2 ; :: thesis: verum

end;

end;

hence a is_dependent_of GPart a ; :: thesis: verum