let x, y be object ; :: thesis: for f being Function-yielding Function st x in dom f & f . x is Function & y in dom <:f:> holds
f .. (x,y) = <:f:> .. (y,x)
let f be Function-yielding Function; :: thesis: ( x in dom f & f . x is Function & y in dom <:f:> implies f .. (x,y) = <:f:> .. (y,x) )
assume that
A1: x in dom f and
f . x is Function and
A2: y in dom <:f:> ; :: thesis: f .. (x,y) = <:f:> .. (y,x)
reconsider g = f . x, h = <:f:> . y as Function ;
A3: dom h = dom f by A2, Th26;
A4: g in rng f by A1, FUNCT_1:def 3;
A5: x in dom h by A1, A3;
y in dom g by A2, A4, Th27;
hence f .. (x,y) = g . y by A1, FUNCT_5:38
.= h . x by A1, A2, Th29
.= <:f:> .. (y,x) by A2, A5, FUNCT_5:38 ;
:: thesis: verum