let Al be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let x be bound_QC-variable of Al; :: thesis:
let CX be Consistent Subset of (CQC-WFF Al); :: thesis:
let JH be Henkin_interpretation of CX; :: thesis:
thus ( JH, valH Al |= Ex (x,p) implies ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) ) :: thesis:

proof

assume JH, valH Al |= Ex (x,p) ; :: thesis:
then consider x1 being Element of HCar Al such that
A1: JH,(valH Al) . (x | x1) |= p by Th9;
A2: HCar Al = bound_QC-variables Al by HENMODEL:def 4;
valH Al = id (bound_QC-variables Al) by HENMODEL:def 6;
then rng (valH Al) = bound_QC-variables Al ;
then consider b being object such that
A3: b in dom (valH Al) and
A4: (valH Al) . b = x1 by A2, FUNCT_1:def 3;
reconsider y = b as bound_QC-variable of Al by A3;
take y ; :: thesis:
thus JH, valH Al |= p . (x,y) by A1, A4, CALCUL_1:24; :: thesis:

end;

thus ( ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) implies JH, valH Al |= Ex (x,p) ) :: thesis:

proof

given y being bound_QC-variable of Al such that A5: JH, valH Al |= p . (x,y) ; :: thesis:
ex x1 being Element of HCar Al st
( (valH Al) . y = x1 & JH,(valH Al) . (x | x1) |= p ) by A5, CALCUL_1:24;
hence JH, valH Al |= Ex (x,p) by Th9; :: thesis:

end;