theorem Th2: :: FUNCOP_1:2

for f, g being Function holds <:f,g:> = <:g,f:> ~