deffunc H₁( set ) -> set = bool (X . $1);
consider p being FinSequence such that
A1: len p = m and
A2: for i being Nat st i in dom p holds
p . i = H₁(i) from FINSEQ_1:sch 2();
reconsider p = p as m -element FinSequence by A1, CARD_1:def 7;
take p ; :: thesis: for i being Nat st i in Seg m holds
p . i is SigmaField of (X . i)

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in Seg m implies p . i is SigmaField of (X . i) )
assume i in Seg m ; :: thesis: p . i is SigmaField of (X . i)
then i in dom p by A1, FINSEQ_1:def 3;
then p . i = bool (X . i) by A2;
hence p . i is SigmaField of (X . i) ; :: thesis: verum

end;