reconsider Y' = Y as Subset of (product (X --> L)) ;
pi Y',i is Subset of ((X --> L) . i) ;
hence pi Y,i is Subset of L by FUNCOP_1:13; :: thesis: verum