let Al be QC-alphabet ; :: thesis:
let PHI be Consistent Subset of (CQC-WFF Al); :: thesis:
let Al2 be Al -expanding QC-alphabet ; :: thesis:
let THETA be Subset of (CQC-WFF Al2); :: thesis:
assume A1: PHI = THETA ; :: thesis:
let A be non empty set ; :: thesis:
let J be interpretation of Al,A; :: thesis:
let v be Element of Valuations_in (Al,A); :: thesis:
assume A2: J,v |= PHI ; :: thesis:
set J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J;
A3: ( dom J = QC-pred_symbols Al & dom ((QC-pred_symbols Al2) --> (empty_rel A)) = QC-pred_symbols Al2 ) by FUNCT_2:def 1;
then dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = (QC-pred_symbols Al) \/ (QC-pred_symbols Al2) by FUNCT_4:def 1;
then A4: dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = QC-pred_symbols Al2 by Th3, XBOOLE_1:12;
J in Funcs ((QC-pred_symbols Al),(relations_on A)) by FUNCT_2:8;
then rng J c= relations_on A by FUNCT_2:92;
then ( (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) c= relations_on A & rng (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) c= (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) ) by FUNCT_4:17, XBOOLE_1:8;
then reconsider J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J as Function of (QC-pred_symbols Al2),(relations_on A) by A4, FUNCT_2:2, XBOOLE_1:1;
A5: J = J2 | (QC-pred_symbols Al) by A3, FUNCT_4:23;
for P2 being Element of QC-pred_symbols Al2
for r being Element of relations_on A holds
( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

let P2 be Element of QC-pred_symbols Al2; :: thesis:
let r be Element of relations_on A; :: thesis:
assume A6: J2 . P2 = r ; :: thesis:

suppose P2 in QC-pred_symbols Al ; :: thesis:

then consider P being QC-pred_symbol of Al such that
A7: P = P2 ;
A8: J . P = r by A3, A6, A7, FUNCT_4:13;
7 + (the_arity_of P2) = P `1 by A7, QC_LANG1:def 8
.= 7 + (the_arity_of P) by QC_LANG1:def 8 ;
hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A8, VALUAT_1:def 5; :: thesis:

end;

suppose not P2 in QC-pred_symbols Al ; :: thesis:

then not P2 in dom J by FUNCT_2:def 1;
then J2 . P2 = ((QC-pred_symbols Al2) --> (empty_rel A)) . P2 by FUNCT_4:11
.= empty_rel A ;
hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A6; :: thesis:

end;

end;

end;

then reconsider J2 = J2 as interpretation of Al2,A by VALUAT_1:def 5;
set a = the Element of A;
set v2 = ((bound_QC-variables Al2) --> the Element of A) +* v;
v in Valuations_in (Al,A) ;
then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then A9: ( dom v = bound_QC-variables Al & dom ((bound_QC-variables Al2) --> the Element of A) = bound_QC-variables Al2 ) by FUNCT_2:92;
then dom (((bound_QC-variables Al2) --> the Element of A) +* v) = (bound_QC-variables Al) \/ (bound_QC-variables Al2) by FUNCT_4:def 1;
then A10: dom (((bound_QC-variables Al2) --> the Element of A) +* v) = bound_QC-variables Al2 by Th4, XBOOLE_1:12;
v in Valuations_in (Al,A) ;
then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then rng v c= A by FUNCT_2:92;
then ( (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) c= A & rng (((bound_QC-variables Al2) --> the Element of A) +* v) c= (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) ) by FUNCT_4:17, XBOOLE_1:8;
then reconsider v2 = ((bound_QC-variables Al2) --> the Element of A) +* v as Function of (bound_QC-variables Al2),A by A10, FUNCT_2:2, XBOOLE_1:1;
A11: v = v2 | (bound_QC-variables Al) by A9, FUNCT_4:23;
v2 in Funcs ((bound_QC-variables Al2),A) by FUNCT_2:8;
then reconsider v2 = v2 as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;
for p2 being Element of CQC-WFF Al2 st p2 in THETA holds
J2,v2 |= p2

let p2 be Element of CQC-WFF Al2; :: thesis:
assume A12: p2 in THETA ; :: thesis:
consider p being Element of CQC-WFF Al such that
A13: ( p = p2 & p in PHI ) by A1, A12;
J,v |= p by A2, A13, CALCUL_1:def 11;
then J2,v2 |= Al2 -Cast p by A5, A11, Th9;
hence J2,v2 |= p2 by A13; :: thesis:

end;

hence ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA by CALCUL_1:def 11; :: thesis: