deffunc H₁( Nat) -> Element of bool (bool (D . $1)) = Trivial-SigmaField (D . $1);
consider f being Function such that
A1: ( dom f = NAT & ( for x being Element of NAT holds f . x = H₁(x) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for n being Nat holds f . n is SigmaField of (D . n)

let n be Nat; :: thesis: f . n is SigmaField of (D . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
f . n1 = Trivial-SigmaField (D . n1) by A1;
hence f . n is SigmaField of (D . n) ; :: thesis: verum

end;

then reconsider f = f as SigmaField_sequence of D by Def8;
take f ; :: thesis: for n being Nat holds f . n = Trivial-SigmaField (D . n)

now :: thesis: for n being Nat holds f . n = Trivial-SigmaField (D . n)

let n be Nat; :: thesis: f . n = Trivial-SigmaField (D . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
f . n1 = Trivial-SigmaField (D . n1) by A1;
hence f . n = Trivial-SigmaField (D . n) ; :: thesis: verum

end;

hence for n being Nat holds f . n = Trivial-SigmaField (D . n) ; :: thesis: verum