let x, y be set ; :: thesis: for f being 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; :: 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
A2: f . x is Function and
A3: y in dom <:f:> ; :: thesis: f .. (x,y) = <:f:> .. (y,x)
reconsider g = f . x, h = <:f:> . y as Function by A2, A3, Th50;
A4: dom h = f " (SubFuncs (rng f)) by A3, Th51;
A5: g in rng f by A1, FUNCT_1:def 3;
then g in SubFuncs (rng f) by Def1;
then A6: x in dom h by A1, A4, FUNCT_1:def 7;
y in dom g by A3, A5, Th52;
hence f .. (x,y) = g . y by A1, FUNCT_5:38
.= h . x by A1, A3, Th54
.= <:f:> .. (y,x) by A3, A6, FUNCT_5:38 ;
:: thesis: verum