let x, y, X be set ; :: thesis: for f being Function
for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds
Swap (A,x,y) = A * f
let f be Function; :: thesis: for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds
Swap (A,x,y) = A * f
let A be array; :: thesis: ( x in X & y in X & f = Swap ((id X),x,y) & X = dom A implies Swap (A,x,y) = A * f )
assume that
A1: ( x in X & y in X ) and
A2: ( f = Swap ((id X),x,y) & X = dom A ) ; :: thesis: Swap (A,x,y) = A * f
set g = id X;
set s = Swap (A,x,y);
A3: ( dom (id X) = X & rng (id X) = X ) ;
then A4: ( dom f = X & rng f = X ) by A2, FUNCT_7:99, FUNCT_7:103;
A5: dom (Swap (A,x,y)) = dom A by FUNCT_7:99;
A6: dom (A * f) = dom f by A2, A4, RELAT_1:27;

now :: thesis: for z being object st z in X holds
(Swap (A,x,y)) . z = (A * f) . z

let z be object ; :: thesis: ( z in X implies (Swap (A,x,y)) . z = (A * f) . z )
assume A7: z in X ; :: thesis: (Swap (A,x,y)) . z = (A * f) . z
A8: ( (id X) . x = x & (id X) . y = y & (id X) . z = z ) by A1, A7, FUNCT_1:17;
( z = x or z = y or ( z <> x & z <> y ) ) ;
then ( ( (Swap (A,x,y)) . z = A . y & f . z = (id X) . y ) or ( (Swap (A,x,y)) . z = A . x & f . z = (id X) . x ) or ( (Swap (A,x,y)) . z = A . z & f . z = (id X) . z ) ) by A1, A2, A3, Th29, Th31, Th33;
hence (Swap (A,x,y)) . z = (A * f) . z by A7, A8, A4, FUNCT_1:13; :: thesis: verum

end;

hence Swap (A,x,y) = A * f by A2, A4, A5, A6; :: thesis: verum