reconsider Y' = Y as Subset of ;
pi Y',i is Subset of ;
hence pi Y,i is Subset of by FUNCOP_1:13; :: thesis: verum