let V be CTLModel; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V
for f1, f2 being Function of CTL_WFF ,the carrier of V st f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai holds
f1 = f2
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: for f1, f2 being Function of CTL_WFF ,the carrier of V st f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai holds
f1 = f2
let f1, f2 be Function of CTL_WFF ,the carrier of V; :: thesis: ( f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai implies f1 = f2 )
assume that
A1: f1 is-Evaluation-for Kai and
A2: f2 is-Evaluation-for Kai ; :: thesis: f1 = f2
for H being set st H in CTL_WFF holds
f1 . H = f2 . H

proof

let H be set ; :: thesis: ( H in CTL_WFF implies f1 . H = f2 . H )
assume H in CTL_WFF ; :: thesis: f1 . H = f2 . H
then reconsider H = H as CTL-formula by Th1;
set n = len H;
A3: f2 is-PreEvaluation-for len H,Kai by A2, Lm26;
f1 is-PreEvaluation-for len H,Kai by A1, Lm26;
hence f1 . H = f2 . H by A3, Lm27; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:18; :: thesis: verum