let x, X, y 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
Z0: ( x in X & y in X ) and
Z1: ( 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);
A0: ( dom (id X) = X & rng (id X) = X ) by RELAT_1:45;
then A1: ( dom f = X & rng f = X ) by Z1, FUNCT_7:99, FUNCT_7:103;
A2: dom (Swap (A,x,y)) = dom A by FUNCT_7:99;
A3: dom (A * f) = dom f by Z1, A1, RELAT_1:27;

now

let z be set ; :: thesis: ( z in X implies (Swap (A,x,y)) . z = (A * f) . z )
assume A4: z in X ; :: thesis: (Swap (A,x,y)) . z = (A * f) . z
A6: ( (id X) . x = x & (id X) . y = y & (id X) . z = z ) by Z0, A4, 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 Z0, Z1, A0, TSa, TSb, TSc;
hence (Swap (A,x,y)) . z = (A * f) . z by A4, A6, A1, FUNCT_1:13; :: thesis: verum

end;

hence Swap (A,x,y) = A * f by Z1, A1, A2, A3, FUNCT_1:2; :: thesis: verum