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_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )
let w be Element of Inf_seq AtomicFamily; :: thesis: for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )
set LN = LTLNodes v;
let f be Function of (LTLNodes v),(LTLNodes v); :: thesis: ( f is_succ_homomorphism v,w implies for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) ) )
assume A1: f is_succ_homomorphism v,w ; :: thesis: for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )
then A2: f is_homomorphism v,w ;
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )

proof

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

proof

let k be Nat; :: thesis: ( ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) implies ( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) ) )
assume A5: for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ; :: thesis: ( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )
set y = (f |** k) . x;
A6: (f |** k) . x in LTLNodes v by A3, FUNCT_2:5;
A7: (f |** (k + 1)) . x = (f * (f |** k)) . x by FUNCT_7:71
.= f . ((f |** k) . x) by A3, FUNCT_2:15 ;
( not CastNode (((f |** k) . x),v) is elementary & w |= * (CastNode (((f |** k) . x),v)) ) by A2, A3, A4, A5, Th47;
hence ( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) ) by A1, A6, A7; :: thesis: verum

end;

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

end;

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