defpred S3[ object , object ] means for p being SCPartialNominativePredicate of V,A st p = $1 holds
for f being Function st f = $2 holds
( dom f = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) ) ) );
A1: for x being object st x in Pr (ND (V,A)) holds
ex y being object st
( y in Pr (ND (V,A)) & S3[x,y] )
proof
let x be object ; :: thesis: ( x in Pr (ND (V,A)) implies ex y being object st
( y in Pr (ND (V,A)) & S3[x,y] ) )
assume x in Pr (ND (V,A)) ; :: thesis: ex y being object st
( y in Pr (ND (V,A)) & S3[x,y] )
then reconsider X = x as PartFunc of (ND (V,A)),BOOLEAN by PARTFUN1:46;
defpred S4[ object , object ] means for d being TypeSCNominativeData of V,A st d = $1 holds
( ( S1[d,X] implies $2 = TRUE ) & ( S2[d,X] implies $2 = FALSE ) );
A2: for a being object st a in H1(X) holds
ex b being object st
( b in BOOLEAN & S4[a,b] )
proof
let a be object ; :: thesis: ( a in H1(X) implies ex b being object st
( b in BOOLEAN & S4[a,b] ) )
assume a in H1(X) ; :: thesis: ex b being object st
( b in BOOLEAN & S4[a,b] )
then consider d being TypeSCNominativeData of V,A such that
A3: a = d and
A4: ( S1[d,X] or S2[d,X] ) ;
per cases ( S1[d,X] or S2[d,X] ) by A4;
suppose A5: S1[d,X] ; :: thesis: ex b being object st
( b in BOOLEAN & S4[a,b] )
take TRUE ; :: thesis: ( TRUE in BOOLEAN & S4[a, TRUE ] )
thus ( TRUE in BOOLEAN & S4[a, TRUE ] ) by A3, A5; :: thesis: verum
end;
suppose A6: S2[d,X] ; :: thesis: ex b being object st
( b in BOOLEAN & S4[a,b] )
take FALSE ; :: thesis: ( FALSE in BOOLEAN & S4[a, FALSE ] )
thus ( FALSE in BOOLEAN & S4[a, FALSE ] ) by A3, A6; :: thesis: verum
end;
end;
end;
consider g being Function such that
A7: dom g = H1(X) and
A8: rng g c= BOOLEAN and
A9: for x being object st x in H1(X) holds
S4[x,g . x] from FUNCT_1:sch 6(A2);
 take g ; :: thesis: ( g in Pr (ND (V,A)) & S3[x,g] )
H1(X) c= ND (V,A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(X) or x in ND (V,A) )
assume x in H1(X) ; :: thesis: x in ND (V,A)
then ex d being TypeSCNominativeData of V,A st
( d = x & ( S1[d,X] or S2[d,X] ) ) ;
hence x in ND (V,A) ; :: thesis: verum
end;
then g is PartFunc of (ND (V,A)),BOOLEAN by A7, A8, RELSET_1:4;
hence g in Pr (ND (V,A)) by PARTFUN1:45; :: thesis: S3[x,g]
let p be SCPartialNominativePredicate of V,A; :: thesis: ( p = x implies for f being Function st f = g holds
( dom f = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) ) ) ) )
assume A10: p = x ; :: thesis: for f being Function st f = g holds
( dom f = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) ) ) )
let f be Function; :: thesis: ( f = g implies ( dom f = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) ) ) ) )
assume A11: f = g ; :: thesis: ( dom f = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) ) ) )
thus dom f = H1(p) by A7, A10, A11; :: thesis: for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) )
let d be TypeSCNominativeData of V,A; :: thesis: ( ( S1[d,p] implies f . d = TRUE ) & ( S2[d,p] implies f . d = FALSE ) )
hereby :: thesis: ( S2[d,p] implies f . d = FALSE )
assume A12: S1[d,p] ; :: thesis: f . d = TRUE
then d in H1(X) by A10;
hence f . d = TRUE by A9, A10, A11, A12; :: thesis: verum
end;
assume A13: S2[d,p] ; :: thesis: f . d = FALSE
then d in H1(X) by A10;
hence f . d = FALSE by A9, A10, A11, A13; :: thesis: verum
end;
consider F being Function of (Pr (ND (V,A))),(Pr (ND (V,A))) such that
A14: for x being object st x in Pr (ND (V,A)) holds
S3[x,F . x] from FUNCT_2:sch 1(A1);
 take F ; :: thesis: for p being SCPartialNominativePredicate of V,A holds
( dom (F . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (F . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (F . p) . d = FALSE ) ) ) )
let p be SCPartialNominativePredicate of V,A; :: thesis: ( dom (F . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (F . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (F . p) . d = FALSE ) ) ) )
p in Pr (ND (V,A)) by PARTFUN1:45;
hence ( dom (F . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (F . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (F . p) . d = FALSE ) ) ) ) by A14; :: thesis: verum