let x, y, X be set ; 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; 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; ( 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 )
; 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 for z being object st z in X holds
(Swap (A,x,y)) . z = (A * f) . zlet z be
object ;
( z in X implies (Swap (A,x,y)) . z = (A * f) . z )assume A7:
z in X
;
(Swap (A,x,y)) . z = (A * f) . zA8:
(
(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;
verum end;
hence
Swap (A,x,y) = A * f
by A2, A4, A5, A6; verum