set A = { (tau1 . p) where p is Element of LTLB_WFF : p in X } ;

deffunc H_{3}( Element of LTLB_WFF ) -> Element of bool LTLB_WFF = tau1 . X;

A1: for x being set st x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } holds

x is finite_{3}(p) where p is Element of LTLB_WFF : p in X } ;

A2: X is finite ;

A3: { H_{3}(p) where p is Element of LTLB_WFF : p in X } is finite
from FRAENKEL:sch 21(A2);

tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X } by Th15;

hence tau X is finite by A3, FINSET_1:7, A1; :: thesis: verum

deffunc H

A1: for x being set st x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } holds

x is finite

proof

set B = { H
let x be set ; :: thesis: ( x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } implies x is finite )

assume x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x is finite

then ex p being Element of LTLB_WFF st

( x = tau1 . p & p in X ) ;

hence x is finite ; :: thesis: verum

end;assume x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x is finite

then ex p being Element of LTLB_WFF st

( x = tau1 . p & p in X ) ;

hence x is finite ; :: thesis: verum

A2: X is finite ;

A3: { H

tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X } by Th15;

hence tau X is finite by A3, FINSET_1:7, A1; :: thesis: verum