let H be LTL-formula; :: thesis: ex L being FinSequence st Subformulae H = rng L
defpred S₁[ LTL-formula] means ex L being FinSequence st Subformulae $1 = rng L;
A1: for H being LTL-formula st H is atomic holds
S₁[H]

proof

let H be LTL-formula; :: thesis: ( H is atomic implies S₁[H] )
assume B1: H is atomic ; :: thesis: S₁[H]
set L = <*H*>;
take <*H*> ; :: thesis: Subformulae H = rng <*H*>
rng <*H*> = {H} by LemFinSeq01
.= Subformulae H by B1, LemSubformulae03 ;
hence Subformulae H = rng <*H*> ; :: thesis: verum

end;

A2: for H being LTL-formula st ( H is negative or H is next ) & S₁[ the_argument_of H] holds
S₁[H]

proof

let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) & S₁[ the_argument_of H] implies S₁[H] )
assume that
B1: ( H is negative or H is next ) and
B2: S₁[ the_argument_of H] ; :: thesis: S₁[H]
consider L1 being FinSequence such that
B3: Subformulae (the_argument_of H) = rng L1 by B2;
set L = L1 ^ <*H*>;
take L1 ^ <*H*> ; :: thesis: Subformulae H = rng (L1 ^ <*H*>)
rng (L1 ^ <*H*>) = (rng L1) \/ (rng <*H*>) by FINSEQ_1:44
.= (Subformulae (the_argument_of H)) \/ {H} by B3, LemFinSeq01
.= Subformulae H by LemSubformulae01, B1 ;
hence Subformulae H = rng (L1 ^ <*H*>) ; :: thesis: verum

end;

A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] holds
S₁[H]

proof

let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] implies S₁[H] )
assume that
B1: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) and
B2: S₁[ the_left_argument_of H] and
B3: S₁[ the_right_argument_of H] ; :: thesis: S₁[H]
consider L1 being FinSequence such that
B4: Subformulae (the_left_argument_of H) = rng L1 by B2;
consider L2 being FinSequence such that
B5: Subformulae (the_right_argument_of H) = rng L2 by B3;
set L = (L1 ^ L2) ^ <*H*>;
take (L1 ^ L2) ^ <*H*> ; :: thesis: Subformulae H = rng ((L1 ^ L2) ^ <*H*>)
B6: rng (L1 ^ L2) = (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H)) by B4, B5, FINSEQ_1:44;
rng ((L1 ^ L2) ^ <*H*>) = (rng (L1 ^ L2)) \/ (rng <*H*>) by FINSEQ_1:44
.= ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by B6, LemFinSeq01
.= Subformulae H by LemSubformulae02, B1 ;
hence Subformulae H = rng ((L1 ^ L2) ^ <*H*>) ; :: thesis: verum

end;

for H being LTL-formula holds S₁[H] from MODELC_2:sch 1(A1, A2, A3);
hence ex L being FinSequence st Subformulae H = rng L ; :: thesis: verum