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 A1: ( x in dom f & f . x is Function & y in dom <:f:> ) ; :: thesis: f .. x,y = <:f:> .. y,x
then reconsider g = f . x, h = <:f:> . y as Function by Th50;
g in rng f by A1, FUNCT_1:def 5;
then A2: ( y in dom g & dom h = f " (SubFuncs (rng f)) & g in SubFuncs (rng f) ) by A1, Def1, Th51, Th52;
then A3: x in dom h by A1, FUNCT_1:def 13;
thus f .. x,y = g . y by A1, A2, FUNCT_5:45
.= h . x by A1, Th54
.= <:f:> .. y,x by A1, A3, FUNCT_5:45 ; :: thesis: verum