let U be Universe; :: thesis: for X being set
for n being non zero Nat st Funcs ((Seg n),{X}) is Element of U holds
X is Element of U
let X be set ; :: thesis: for n being non zero Nat st Funcs ((Seg n),{X}) is Element of U holds
X is Element of U
let n be non zero Nat; :: thesis: ( Funcs ((Seg n),{X}) is Element of U implies X is Element of U )
assume A1: Funcs ((Seg n),{X}) is Element of U ; :: thesis: X is Element of U
set R = (Seg n) --> X;
reconsider f = (Seg n) --> X as Function of (Seg n),{X} ;
f in Funcs ((Seg n),{X}) by FUNCT_2:8;
then f is Element of U by A1, CLASSES4:def 1;
then {X} is Element of U by CLASSES4:40;
hence X is Element of U by Th18; :: thesis: verum