deffunc H_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 4();

reconsider f = f as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;

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

consider f being Function such that

A1: ( dom f = NAT & ( for x being Element of NAT holds f . x = H

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)

then reconsider f = f as SigmaField_sequence of D by Def8;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;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

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)

hence
for n being Nat holds f . n = Trivial-SigmaField (D . n)
; :: thesis: verumlet 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;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