deffunc H_{1}( set ) -> set = bool (X . n);

consider p being FinSequence such that

A1: len p = n and

A2: for i being Nat st i in dom p holds

p . i = H_{1}(i)
from FINSEQ_1:sch 2();

reconsider p = p as n -element FinSequence by A1, CARD_1:def 7;

take p ; :: thesis: ( p is SemiringFamily of X & p is cap-closed-yielding )

hence ( p is SemiringFamily of X & p is cap-closed-yielding ) ; :: thesis: verum

consider p being FinSequence such that

A1: len p = n and

A2: for i being Nat st i in dom p holds

p . i = H

reconsider p = p as n -element FinSequence by A1, CARD_1:def 7;

take p ; :: thesis: ( p is SemiringFamily of X & p is cap-closed-yielding )

now :: thesis: for i being Nat st i in Seg n holds

p . i is semiring_of_sets of (X . i)

then reconsider p = p as SemiringFamily of X by Def2;p . i is semiring_of_sets of (X . i)

let i be Nat; :: thesis: ( i in Seg n implies p . i is semiring_of_sets of (X . i) )

assume A3: i in Seg n ; :: thesis: p . i is semiring_of_sets of (X . i)

reconsider Xi = X . i as set ;

A4: bool Xi is semiring_of_sets of Xi by SRINGS_2:5;

i in dom p by A3, A1, FINSEQ_1:def 3;

hence p . i is semiring_of_sets of (X . i) by A2, A4; :: thesis: verum

end;assume A3: i in Seg n ; :: thesis: p . i is semiring_of_sets of (X . i)

reconsider Xi = X . i as set ;

A4: bool Xi is semiring_of_sets of Xi by SRINGS_2:5;

i in dom p by A3, A1, FINSEQ_1:def 3;

hence p . i is semiring_of_sets of (X . i) by A2, A4; :: thesis: verum

now :: thesis: for i being Nat st i in Seg n holds

p . i is cap-closed

then
p is cap-closed-yielding
;p . i is cap-closed

let i be Nat; :: thesis: ( i in Seg n implies p . i is cap-closed )

assume i in Seg n ; :: thesis: p . i is cap-closed

then i in dom p by A1, FINSEQ_1:def 3;

then p . i = bool (X . i) by A2;

hence p . i is cap-closed ; :: thesis: verum

end;assume i in Seg n ; :: thesis: p . i is cap-closed

then i in dom p by A1, FINSEQ_1:def 3;

then p . i = bool (X . i) by A2;

hence p . i is cap-closed ; :: thesis: verum

hence ( p is SemiringFamily of X & p is cap-closed-yielding ) ; :: thesis: verum