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 & 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
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_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
w |= * (CastNode ((f |** k) . 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 & 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
w |= * (CastNode ((f |** k) . x),v) )
assume f is_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
w |= * (CastNode ((f |** k) . x),v)
then A1: for y being set st y in LTLNodes v & not CastNode y,v is elementary & w |= * (CastNode y,v) holds
w |= * (CastNode (f . y),v) by defHom;
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
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
w |= * (CastNode ((f |** k) . x),v) )
assume B1: ( x in LTLNodes v & 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
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
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 w |= * (CastNode ((f |** k) . x),v) )
assume C1: for i being Nat st i <= k holds
not CastNode ((f |** i) . x),v is elementary ; :: thesis: w |= * (CastNode ((f |** k) . x),v)
defpred S₁[ Nat] means ( ( for i being Nat st i <= $1 holds
not CastNode ((f |** i) . x),v is elementary ) implies w |= * (CastNode ((f |** $1) . x),v) );
C2: S₁[ 0 ]

proof

assume for i being Nat st i <= 0 holds
not CastNode ((f |** i) . x),v is elementary ; :: thesis: w |= * (CastNode ((f |** 0 ) . x),v)
f |** 0 = id (LTLNodes v) by FUNCT_7:86;
hence w |= * (CastNode ((f |** 0 ) . x),v) by B1, FUNCT_1:35; :: thesis: verum

end;

C3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume D1: S₁[m] ; :: thesis: S₁[m + 1]
S₁[m + 1]

proof

assume E1: for i being Nat st i <= m + 1 holds
not CastNode ((f |** i) . x),v is elementary ; :: thesis: w |= * (CastNode ((f |** (m + 1)) . x),v)
set y = (f |** m) . x;
E2: m <= m + 1 by NAT_1:13;
then E3: not CastNode ((f |** m) . x),v is elementary by E1;
E4: w |= * (CastNode ((f |** m) . x),v) by E1, E2, D1, XXREAL_0:2;
(f |** (m + 1)) . x = (f * (f |** m)) . x by FUNCT_7:73
.= f . ((f |** m) . x) by B1, FUNCT_2:21 ;
hence w |= * (CastNode ((f |** (m + 1)) . x),v) by A1, E3, E4, B1, FUNCT_2:7; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(C2, C3);
hence w |= * (CastNode ((f |** k) . x),v) by C1; :: 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
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
w |= * (CastNode ((f |** k) . x),v) ; :: thesis: verum