let V be LTLModelStr ; :: thesis: for Kai being Function of atomic_LTL ,the BasicAssign of V
for f1, f2 being Function of LTL_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_LTL ,the BasicAssign of V; :: thesis: for f1, f2 being Function of LTL_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 LTL_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 LTL_WFF holds
f1 . H = f2 . H

proof

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

end;

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