let UN be Universe; :: thesis: for X being set st X in UN holds
for s being FinSequence of X holds s in UN
let X be set ; :: thesis: ( X in UN implies for s being FinSequence of X holds s in UN )
assume A1: X in UN ; :: thesis: for s being FinSequence of X holds s in UN
let s be FinSequence of X; :: thesis: s in UN
consider n being Nat such that
A2: dom s = Seg n by FINSEQ_1:def 2;
rng s c= X ;
then A3: s is Function of (dom s),X by FUNCT_2:2;
Seg n in UN by Th57;
then [:(Seg n),X:] in UN by A1, CLASSES2:61;
hence s in UN by A3, A2, Th13; :: thesis: verum