let s be Element of S; :: thesis: s is PartFunc of ,
thus s is PartFunc of , by PARTFUN1:120; :: thesis: verum