deffunc H_{1}( Element of NAT ) -> set = { f where f is Element of Funcs ((Seg $1),(Seg ($1 + 1))) : @ f is increasing } ;

consider F being ManySortedSet of NAT such that

A1: for n being Element of NAT holds F . n = H_{1}(n)
from PBOOLE:sch 5();

reconsider F = F as SetSequence ;

take F ; :: thesis: for n being Nat holds F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

let n be Nat; :: thesis: F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

n in NAT by ORDINAL1:def 12;

hence F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A1; :: thesis: verum

consider F being ManySortedSet of NAT such that

A1: for n being Element of NAT holds F . n = H

reconsider F = F as SetSequence ;

take F ; :: thesis: for n being Nat holds F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

let n be Nat; :: thesis: F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

n in NAT by ORDINAL1:def 12;

hence F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A1; :: thesis: verum