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 that
A1: x in dom f and
A2: 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, A2, FUNCT_1:35;
then reconsider p = ((id (dom f)) +* x,y) +* y,x as Permutation of (dom f) by A1, A2, Th112;
set pk = (id (dom f)) +* x,y;
set fr = f * p;
set fk = f +* x,(f . y);
take p ; :: thesis: (f +* x,(f . y)) +* y,(f . x) = f * p
set fl = (f +* x,(f . y)) +* y,(f . x);
A3: dom (id (dom f)) = dom f by FUNCT_1:34;
A4: dom (f +* x,(f . y)) = dom ((f +* x,(f . y)) +* y,(f . x)) by Th32;
A5: dom p = dom ((id (dom f)) +* x,y) by Th32;
A6: dom ((id (dom f)) +* x,y) = dom (id (dom f)) by Th32;
A7: dom f = dom (f +* x,(f . y)) by Th32;

now

thus dom f = dom ((f +* x,(f . y)) +* y,(f . x)) by A4, 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 A5, A6, A3, 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 A8: z in dom f ; :: thesis: ((f +* x,(f . y)) +* y,(f . x)) . b₁ = (f * p) . b₁

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

suppose A9: 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 A10: 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 A9, Th34
.= f . y by A8, A10, Th33
.= f . (((id (dom f)) +* x,y) . x) by A1, A3, Th33
.= f . (p . x) by A9, Th34
.= (f * p) . z by A5, A6, A3, A8, A10, FUNCT_1:23 ;
:: thesis: verum

end;

suppose A11: 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 A7, A8, Th33
.= f . (p . y) by A2, A6, A3, Th33
.= (f * p) . z by A5, A6, A3, A8, A11, FUNCT_1:23 ;
:: thesis: verum

end;

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

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

end;

end;

end;

end;

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

A15: x = (id (dom f)) . x by A1, FUNCT_1:34;
( f +* x,(f . y) = f & id (dom f) = (id (dom f)) +* x,((id (dom f)) . y) ) by A14, Th37;
hence ((f +* x,(f . y)) +* y,(f . x)) . z = (f * p) . z by 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