let F1, F2 be Function; :: thesis: ( ( for a being set holds
( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds
( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) implies F1 = F2 )
assume that
A15: for a being set holds
( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) and
A16: for a being set holds
( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; :: thesis: F1 = F2

now :: thesis: for a being set holds
( a in F1 iff a in F2 )

let a be set ; :: thesis: ( a in F1 iff a in F2 )
( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) by A15;
hence ( a in F1 iff a in F2 ) by A16; :: thesis: verum

end;

hence F1 = F2 by TARSKI:1; :: thesis: verum