set LS = LTLStates v;
deffunc H₁( Nat, set ) -> strict elementary LTLnode of v = chosen_next (Shift w,$1),v,U,(CastNode $2,v);
deffunc H₂( set , set ) -> strict elementary LTLnode of v = chosen_next (Shift w,(CastNat $1)),v,U,(CastNode $2,v);
A1: for f, g being Function of NAT ,(LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) holds
f = g

proof

let f, g be Function of NAT ,(LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) implies f = g )
assume that
B1: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) and
B2: ( g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) ) ; :: thesis: f = g
B4: ( dom f = NAT & f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) by B1, FUNCT_2:def 1;
B5: ( dom g = NAT & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) ) by B2, FUNCT_2:def 1;
defpred S₁[ Nat] means f . $1 = g . $1;
B601: S₁[ 0 ] by B1, B2;
B602: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume C1: S₁[k] ; :: thesis: S₁[k + 1]
f . (k + 1) = H₂(k,g . k) by B1, C1
.= g . (k + 1) by B2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(B601, B602);
then for x being set st x in dom f holds
f . x = g . x ;
hence f = g by B4, B5, FUNCT_1:9; :: thesis: verum

end;

for f, g being Function of NAT ,(LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) holds
f = g

proof

let f, g be Function of NAT ,(LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) implies f = g )
assume that
B1: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) and
B2: ( g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) ) ; :: thesis: f = g
B3: for n being Nat holds f . (n + 1) = H₂(n,f . n)

proof

let n be Nat; :: thesis: f . (n + 1) = H₂(n,f . n)
f . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (f . n),v) by B1;
hence f . (n + 1) = H₂(n,f . n) by MODELC_2:def 1; :: thesis: verum

end;

for n being Nat holds g . (n + 1) = H₂(n,g . n)

proof

let n be Nat; :: thesis: g . (n + 1) = H₂(n,g . n)
g . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (g . n),v) by B2;
hence g . (n + 1) = H₂(n,g . n) by MODELC_2:def 1; :: thesis: verum

end;

hence f = g by B1, B2, B3, A1; :: thesis: verum

end;

hence for b₁, b₂ being sequence of (LTLStates v) st b₁ . 0 = init v & ( for n being Nat holds b₁ . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (b₁ . n),v) ) & b₂ . 0 = init v & ( for n being Nat holds b₂ . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (b₂ . n),v) ) holds
b₁ = b₂ ; :: thesis: verum