deffunc H1( 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 = H1(i) from reconsider p = p as n -element FinSequence by ;
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)
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 ;
hence p . i is semiring_of_sets of (X . i) by A2, A4; :: thesis: verum
end;
then reconsider p = p as SemiringFamily of X by Def2;
now :: thesis: for i being Nat st i in Seg n holds
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 ;
then p . i = bool (X . i) by A2;
hence p . i is cap-closed ; :: thesis: verum
end;
then p is cap-closed-yielding ;
hence ( p is SemiringFamily of X & p is cap-closed-yielding ) ; :: thesis: verum