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 object st H in CTL_WFF holds
f1 . H = f2 . H

proof

let H be object ; :: 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;
f1 is-PreEvaluation-for len H,Kai by A1;
hence f1 . H = f2 . H by A3, Lm26; :: thesis: verum

end;

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