let f be Function; :: thesis: for x, y being set st x in dom f & y in dom f holds
ex p being Permutation of (dom f) st (f +* x,(f . y)) +* y,(f . x) = f * p
let x, y be set ; :: thesis: ( x in dom f & y in dom f implies ex p being Permutation of (dom f) st (f +* x,(f . y)) +* y,(f . x) = f * p )
assume A1: ( x in dom f & y in dom f ) ; :: thesis: ex p being Permutation of (dom f) st (f +* x,(f . y)) +* y,(f . x) = f * p
set i = id (dom f);
( (id (dom f)) . x = x & (id (dom f)) . y = y ) by A1, FUNCT_1:35;
then reconsider p = ((id (dom f)) +* x,y) +* y,x as Permutation of (dom f) by A1, Th112;
take p ; :: thesis: (f +* x,(f . y)) +* y,(f . x) = f * p
set fk = f +* x,(f . y);
set fl = (f +* x,(f . y)) +* y,(f . x);
set fr = f * p;
set pk = (id (dom f)) +* x,y;
A2: dom f = dom (f +* x,(f . y)) by Th32;
A3: dom (f +* x,(f . y)) = dom ((f +* x,(f . y)) +* y,(f . x)) by Th32;
A4: dom p = dom ((id (dom f)) +* x,y) by Th32;
A5: dom ((id (dom f)) +* x,y) = dom (id (dom f)) by Th32;
A6: dom (id (dom f)) = dom f by FUNCT_1:34;

now

thus dom f = dom ((f +* x,(f . y)) +* y,(f . x)) by A3, Th32; :: thesis: ( dom f = dom (f * p) & ( for z being set st z in dom f holds
((f +* x,(f . y)) +* y,(f . x)) . b₂ = (f * p) . b₂ ) )
rng p = dom f by FUNCT_2:def 3;
hence dom f = dom (f * p) by A4, A5, A6, RELAT_1:46; :: thesis: for z being set st z in dom f holds
((f +* x,(f . y)) +* y,(f . x)) . b₂ = (f * p) . b₂
let z be set ; :: thesis: ( z in dom f implies ((f +* x,(f . y)) +* y,(f . x)) . b₁ = (f * p) . b₁ )
assume A7: z in dom f ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . b₁ = (f * p) . b₁

per cases ( x <> y or x = y ) ;

suppose A8: x <> y ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . b₁ = (f * p) . b₁

thus ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z :: thesis: verum

proof

per cases ( z = x or z = y or ( z <> x & z <> y ) ) ;

suppose A9: z = x ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z

hence ((f +* x,(f . y)) +* y,(f . x)) . z = (f +* x,(f . y)) . z by A8, Th34
.= f . y by A7, A9, Th33
.= f . (((id (dom f)) +* x,y) . x) by A1, A6, Th33
.= f . (p . x) by A8, Th34
.= (f * p) . z by A4, A5, A6, A7, A9, FUNCT_1:23 ;
:: thesis: verum

end;

suppose A10: z = y ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z

hence ((f +* x,(f . y)) +* y,(f . x)) . z = f . x by A2, A7, Th33
.= f . (p . y) by A1, A5, A6, Th33
.= (f * p) . z by A4, A5, A6, A7, A10, FUNCT_1:23 ;
:: thesis: verum

end;

suppose A11: ( z <> x & z <> y ) ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z

then A12: p . z = ((id (dom f)) +* x,y) . z by Th34
.= (id (dom f)) . z by A11, Th34
.= z by A7, FUNCT_1:35 ;
thus ((f +* x,(f . y)) +* y,(f . x)) . z = (f +* x,(f . y)) . z by A11, Th34
.= f . (p . z) by A11, A12, Th34
.= (f * p) . z by A4, A5, A6, A7, FUNCT_1:23 ; :: thesis: verum

end;

end;

end;

end;

suppose A13: x = y ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . b₁ = (f * p) . b₁

then A14: f +* x,(f . y) = f by Th37;
A15: x = (id (dom f)) . x by A1, FUNCT_1:34;
id (dom f) = (id (dom f)) +* x,((id (dom f)) . y) by A13, Th37;
hence ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z by A13, A14, A15, RELAT_1:78; :: thesis: verum

end;

end;

end;

hence (f +* x,(f . y)) +* y,(f . x) = f * p by FUNCT_1:9; :: thesis: verum