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