deffunc H₁( 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₁(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