let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V
for f1, f2 being Function of LTL_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_LTL, the BasicAssign of V; :: thesis: for f1, f2 being Function of LTL_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 LTL_WFF, the carrier of V; :: thesis: ( f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai implies f1 = f2 )
assume A1: ( f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai ) ; :: thesis: f1 = f2
for H being object st H in LTL_WFF holds
f1 . H = f2 . H

proof

let H be object ; :: thesis: ( H in LTL_WFF implies f1 . H = f2 . H )
assume H in LTL_WFF ; :: thesis: f1 . H = f2 . H
then reconsider H = H as LTL-formula by Th1;
set n = len H;
( f1 is-PreEvaluation-for len H,Kai & f2 is-PreEvaluation-for len H,Kai ) by A1;
hence f1 . H = f2 . H by Lm24; :: thesis: verum

end;

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