deffunc H1( 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 = H1(x) ) ) from reconsider f = f as ManySortedSet of NAT by ;
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