consider f being Function of CTL_WFF, the carrier of V such that
A1: f is-Evaluation-for Kai by Th3;
set IT = f . H;
H in CTL_WFF by Th1;
then reconsider IT = f . H as Assign of V by FUNCT_2:5;
take IT ; :: thesis: ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & IT = f . H )
thus ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & IT = f . H ) by A1; :: thesis: verum