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 S1[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S1[x] } as Subset of Y from DOMAIN_1:sch 7();
 defpred S2[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S2[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