let Al be QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being Al -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: for Al2 being Al -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let Al2 be Al -expanding QC-alphabet ; :: thesis: for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let THETA be Subset of (CQC-WFF Al2); :: thesis: ( PHI = THETA implies for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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 )

assume A1: PHI = THETA ; :: thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let A be non empty set ; :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
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

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= PHI implies 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 )
assume A2: J,v |= PHI ; :: thesis: 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
set J2 = (() --> ()) +* J;
A3: ( dom J = QC-pred_symbols Al & dom (() --> ()) = QC-pred_symbols Al2 ) by FUNCT_2:def 1;
then dom ((() --> ()) +* J) = () \/ () by FUNCT_4:def 1;
then A4: dom ((() --> ()) +* J) = QC-pred_symbols Al2 by ;
J in Funcs ((),()) by FUNCT_2:8;
then rng J c= relations_on A by FUNCT_2:92;
then ( (rng (() --> ())) \/ (rng J) c= relations_on A & rng ((() --> ()) +* J) c= (rng (() --> ())) \/ (rng J) ) by ;
then reconsider J2 = (() --> ()) +* J as Function of (),() by ;
A5: J = J2 | () by ;
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 )
proof
let P2 be Element of QC-pred_symbols Al2; :: thesis: 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 r be Element of relations_on A; :: thesis: ( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )
assume A6: J2 . P2 = r ; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )
per cases ( P2 in QC-pred_symbols Al or not P2 in QC-pred_symbols Al ) ;
suppose P2 in QC-pred_symbols Al ; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )
then consider P being QC-pred_symbol of Al such that
A7: P = P2 ;
A8: J . P = r by ;
7 + () = P `1 by
.= 7 + () by QC_LANG1:def 8 ;
hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by ; :: thesis: verum
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 = (() --> the Element of A) +* v;
v in Valuations_in (Al,A) ;
then v in Funcs ((),A) by VALUAT_1:def 1;
then A9: ( dom v = bound_QC-variables Al & dom (() --> the Element of A) = bound_QC-variables Al2 ) by FUNCT_2:92;
then dom ((() --> the Element of A) +* v) = () \/ () by FUNCT_4:def 1;
then A10: dom ((() --> the Element of A) +* v) = bound_QC-variables Al2 by ;
v in Valuations_in (Al,A) ;
then v in Funcs ((),A) by VALUAT_1:def 1;
then rng v c= A by FUNCT_2:92;
then ( (rng (() --> the Element of A)) \/ (rng v) c= A & rng ((() --> the Element of A) +* v) c= (rng (() --> the Element of A)) \/ (rng v) ) by ;
then reconsider v2 = (() --> the Element of A) +* v as Function of (),A by ;
A11: v = v2 | () by ;
v2 in Funcs ((),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
proof
let p2 be Element of CQC-WFF Al2; :: thesis: ( p2 in THETA implies J2,v2 |= p2 )
assume A12: p2 in THETA ; :: thesis: J2,v2 |= p2
consider p being Element of CQC-WFF Al such that
A13: ( p = p2 & p in PHI ) by ;
J,v |= p by ;
then J2,v2 |= Al2 -Cast p by A5, A11, Th9;
hence J2,v2 |= p2 by A13; :: thesis: verum
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: verum