defpred S₁[ object , object ] means ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( $1 = [p,Sub] & p,Sub PQSub $2 );
A1: for a, b1, b2 being object st S₁[a,b1] & S₁[a,b2] holds
b1 = b2

proof

let a, b1, b2 be object ; :: thesis: ( S₁[a,b1] & S₁[a,b2] implies b1 = b2 )
assume that
A2: ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b1 ) and
A3: ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b2 ) ; :: thesis: b1 = b2
consider p1 being QC-formula of A, Sub1 being CQC_Substitution of A such that
A4: a = [p1,Sub1] and
A5: p1,Sub1 PQSub b1 by A2;
consider p2 being QC-formula of A, Sub2 being CQC_Substitution of A such that
A6: a = [p2,Sub2] and
A7: p2,Sub2 PQSub b2 by A3;
A8: p1 = p2 by A4, A6, XTUPLE_0:1;
A9: Sub1 = Sub2 by A4, A6, XTUPLE_0:1;

per cases ( p1 is universal or not p1 is universal ) ;

suppose A10: p1 is universal ; :: thesis: b1 = b2

then b1 = ExpandSub ((bound_in p1),(the_scope_of p1),(RestrictSub ((bound_in p1),p1,Sub1))) by A5;
hence b1 = b2 by A7, A8, A9, A10; :: thesis: verum

end;

suppose A11: not p1 is universal ; :: thesis: b1 = b2

then b1 = {} by A5;
hence b1 = b2 by A7, A8, A11; :: thesis: verum

end;

end;

end;

consider f being Function such that
A12: for a, b being object holds
( [a,b] in f iff ( a in [:(QC-WFF A),(vSUB A):] & S₁[a,b] ) ) from FUNCT_1:sch 1(A1);
take f ; :: thesis: for a being object holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
for c being object holds
( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) )

proof

let c be object ; :: thesis: ( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) )
thus ( c in f implies ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) ) :: thesis: ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f )

proof

assume A13: c in f ; :: thesis: ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b )
then consider a, b being object such that
A14: c = [a,b] by RELAT_1:def 1;
ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b ) by A12, A13, A14;
hence ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) by A14; :: thesis: verum

end;

thus ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f ) by A12; :: thesis: verum

end;

hence for a being object holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; :: thesis: verum