thus ex f being Function st
( dom f = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1); :: thesis: verum