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 5;
then g in SubFuncs (rng f) by Def1;
then A6: x in dom h by A1, A4, FUNCT_1:def 13;
y in dom g by A3, A5, Th52;
hence f .. x,y = g . y by A1, FUNCT_5:45
.= h . x by A1, A3, Th54
.= <:f:> .. y,x by A3, A6, FUNCT_5:45 ;
:: thesis: verum