let i be Nat; :: thesis: ex x being set st x in (sequence_univers . (i + 1)) \ (sequence_univers . i)
assume for x being set holds not x in (sequence_univers . (i + 1)) \ (sequence_univers . i) ; :: thesis: contradiction
then A1: (sequence_univers . (i + 1)) \ (sequence_univers . i) is empty ;
then A2: sequence_univers . (i + 1) = sequence_univers . i by Th105, XBOOLE_1:37;

per cases ( i = 0 or i <> 0 ) ;

suppose A3: i = 0 ; :: thesis: contradiction

GrothendieckUniverse (sequence_univers . 0) = sequence_univers . (0 + 1) by Def9
.= sequence_univers . 0 by A1, A3, Th105, XBOOLE_1:37
.= {} by Def9 ;
hence contradiction ; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: contradiction

then consider m being Nat such that
A4: i = m + 1 by NAT_1:6;
A5: sequence_univers . (i + 1) = UNIVERSE i by Th102;
sequence_univers . i = UNIVERSE m by A4, Th102;
then m = i by A2, A5, CLASSES2:71;
hence contradiction by A4; :: thesis: verum

end;

end;