let C, D be non empty set ; :: thesis: for c1, c2 being Element of C
for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}
let c1, c2 be Element of C; :: thesis: for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}
let f be PartFunc of C,D; :: thesis: ( c1 in dom f & c2 in dom f implies f .: {c1,c2} = {(f /. c1),(f /. c2)} )
assume A1: ( c1 in dom f & c2 in dom f ) ; :: thesis: f .: {c1,c2} = {(f /. c1),(f /. c2)}
hence f .: {c1,c2} = {(f . c1),(f . c2)} by FUNCT_1:118
.= {(f /. c1),(f . c2)} by A1, PARTFUN1:def 8
.= {(f /. c1),(f /. c2)} by A1, PARTFUN1:def 8 ;
:: thesis: verum