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:18;
then reconsider p = ((id (dom f)) +* (x,y)) +* (y,x) as Permutation of (dom f) by A1, A2, Th109;
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 ;
A4: dom (f +* (x,(f . y))) = dom ((f +* (x,(f . y))) +* (y,(f . x))) by Th29;
A5: dom p = dom ((id (dom f)) +* (x,y)) by Th29;
A6: dom ((id (dom f)) +* (x,y)) = dom (id (dom f)) by Th29;
A7: dom f = dom (f +* (x,(f . y))) by Th29;

now :: thesis: ( dom f = dom ((f +* (x,(f . y))) +* (y,(f . x))) & dom f = dom (f * p) & ( for z being object st z in dom f holds
((f +* (x,(f . y))) +* (y,(f . x))) . z = (f * p) . z ) )

thus dom f = dom ((f +* (x,(f . y))) +* (y,(f . x))) by A4, Th29; :: thesis: ( dom f = dom (f * p) & ( for z being object 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, RELAT_1:27; :: thesis: for z being object st z in dom f holds
((f +* (x,(f . y))) +* (y,(f . x))) . b₂ = (f * p) . b₂
let z be object ; :: 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, Th31
.= f . y by A8, A10, Th30
.= f . (((id (dom f)) +* (x,y)) . x) by A1, A3, Th30
.= f . (p . x) by A9, Th31
.= (f * p) . z by A5, A6, A8, A10, FUNCT_1:13 ;
:: 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, Th30
.= f . (p . y) by A2, A6, Th30
.= (f * p) . z by A5, A6, A8, A11, FUNCT_1:13 ;
:: 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 Th31
.= (id (dom f)) . z by A12, Th31
.= z by A8, FUNCT_1:18 ;
thus ((f +* (x,(f . y))) +* (y,(f . x))) . z = (f +* (x,(f . y))) . z by A12, Th31
.= f . (p . z) by A12, A13, Th31
.= (f * p) . z by A5, A6, A8, FUNCT_1:13 ; :: 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:17;
( f +* (x,(f . y)) = f & id (dom f) = (id (dom f)) +* (x,((id (dom f)) . y)) ) by A14, Th34;
hence ((f +* (x,(f . y))) +* (y,(f . x))) . z = (f * p) . z by A14, A15, RELAT_1:52; :: thesis: verum

end;

end;

end;

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