let v be LTL-formula; :: thesis: for w being Element of Inf_seq AtomicFamily
for f being Function of LTLNodes v, LTLNodes v st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)
let w be Element of Inf_seq AtomicFamily ; :: thesis: for f being Function of LTLNodes v, LTLNodes v st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)
set LN = LTLNodes v;
let f be Function of LTLNodes v, LTLNodes v; :: thesis: ( f is_homomorphism v,w implies for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v) )
assume A1: f is_homomorphism v,w ; :: thesis: for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)
for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)

proof

let x be set ; :: thesis: ( x in LTLNodes v & not CastNode x,v is elementary implies for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v) )
assume that
A2: x in LTLNodes v and
not CastNode x,v is elementary ; :: thesis: for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)

proof

let k be Nat; :: thesis: ( not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) implies w |= * (CastNode ((f |** (k + 1)) . x),v) )
assume A3: ( not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) ) ; :: thesis: w |= * (CastNode ((f |** (k + 1)) . x),v)
set y = (f |** k) . x;
A4: (f |** (k + 1)) . x = (f * (f |** k)) . x by FUNCT_7:73
.= f . ((f |** k) . x) by A2, FUNCT_2:21 ;
(f |** k) . x in LTLNodes v by A2, FUNCT_2:7;
hence w |= * (CastNode ((f |** (k + 1)) . x),v) by A1, A3, A4, Def33; :: thesis: verum

end;

hence for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v) ; :: thesis: verum

end;

hence for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v) ; :: thesis: verum