set f = sequence_univers {};
A1: ( dom (sequence_univers {}) = NAT & (sequence_univers {}) . 0 = {} & ( for n being Nat holds (sequence_univers {}) . (n + 1) = GrothendieckUniverse ((sequence_univers {}) . n) ) ) by Def9;
A2: (sequence_univers {}) . 1 = (sequence_univers {}) . (0 + 1)
.= GrothendieckUniverse {} by A1
.= FinSETS by Th45, CLASSES2:56, CLASSES3:21 ;
(sequence_univers {}) . 2 = (sequence_univers {}) . (1 + 1)
.= SETS by Th77, A2, Def9 ;
hence ( {} in rng sequence_univers & FinSETS in rng sequence_univers & SETS in rng sequence_univers ) by A1, A2, FUNCT_1:3; :: thesis: verum