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