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

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