let F1, F2 be Function; :: thesis: ( ( for a being set holds
( a in F1 iff ex p being QC-formula ex Sub being CQC_Substitution 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 ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) implies F1 = F2 )
assume A11: ( ( for a being set holds
( a in F1 iff ex p being QC-formula ex Sub being CQC_Substitution 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 ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) ) ; :: thesis: F1 = F2

now

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

end;

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