theorem Th1: :: AOFA_I00:1

for x, y, z, a, b, c being set st a <> b & b <> c & c <> a holds
ex f being Function st
( f . a = x & f . b = y & f . c = z )