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:71
.= f . ((f |** k) . x) by A2, FUNCT_2:15 ;
(f |** k) . x in LTLNodes v by A2, FUNCT_2:5;
hence w |= * (CastNode (((f |** (k + 1)) . x),v)) by A1, A3, A4; :: 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