let x1, x2 be object ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ) )
proof
let y be object ; :: thesis: ( y in f .: {x1,x2} iff ( y = f . x1 or y = f . x2 ) )
A2: ( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def 2;
thus ( not y in f .: {x1,x2} or y = f . x1 or y = f . x2 ) :: thesis: ( ( y = f . x1 or y = f . x2 ) implies y in f .: {x1,x2} )
proof
assume y in f .: {x1,x2} ; :: thesis: ( y = f . x1 or y = f . x2 )
then ex x being object st
( x in dom f & x in {x1,x2} & y = f . x ) by Def6;
hence ( y = f . x1 or y = f . x2 ) by TARSKI:def 2; :: thesis: verum
end;
assume ( y = f . x1 or y = f . x2 ) ; :: thesis: y in f .: {x1,x2}
hence y in f .: {x1,x2} by A1, A2, Def6; :: thesis: verum
end;
hence f .: {x1,x2} = {(f . x1),(f . x2)} by TARSKI:def 2; :: thesis: verum