let x1, x2 be object ; for f being Function st x1 in dom f & x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}
let f be Function; ( x1 in dom f & x2 in dom f implies f .: {x1,x2} = {(f . x1),(f . x2)} )
assume A1:
( x1 in dom f & x2 in dom f )
; f .: {x1,x2} = {(f . x1),(f . x2)}
for y being object holds
( y in f .: {x1,x2} iff ( y = f . x1 or y = f . x2 ) )
hence
f .: {x1,x2} = {(f . x1),(f . x2)}
by TARSKI:def 2; verum