let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V
for f1, f2 being Function of CTL_WFF ,the Assignations 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 Assignations 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 Assignations 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 A3: H in CTL_WFF ; :: thesis: f1 . H = f2 . H
reconsider H = H as CTL-formula by A3, Th1;
set n = len H;
( f1 is-PreEvaluation-for len H,Kai & f2 is-PreEvaluation-for len H,Kai ) by A1, A2, Lm26;
hence f1 . H = f2 . H by Lm27; :: thesis: verum

end;

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