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 that
A1: c1 in dom f and
A2: c2 in dom f ; :: thesis: f .: {c1,c2} = {(f /. c1),(f /. c2)}
thus f .: {c1,c2} = {(f . c1),(f . c2)} by A1, A2, FUNCT_1:60
.= {(f /. c1),(f . c2)} by A1, PARTFUN1:def 6
.= {(f /. c1),(f /. c2)} by A2, PARTFUN1:def 6 ; :: thesis: verum