let X be non empty set ; :: thesis: for f being sequence of X
for i, j being Nat ex g being sequence of X st
( ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i )
let f be sequence of X; :: thesis: for i, j being Nat ex g being sequence of X st
( ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i )
let i, j be Nat; :: thesis: ex g being sequence of X st
( ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i )
defpred S₁[ object , object ] means ( ( $1 <> i & $1 <> j implies $2 = f . $1 ) & ( $1 = i implies $2 = f . j ) & ( $1 = j implies $2 = f . i ) );
A1: for n being Element of NAT ex x being Element of X st S₁[n,x]

proof

let n be Element of NAT ; :: thesis: ex x being Element of X st S₁[n,x]

per cases ( ( n <> i & n <> j ) or n = i or n = j ) ;

suppose A2: ( n <> i & n <> j ) ; :: thesis: ex x being Element of X st S₁[n,x]

reconsider x = f . n as Element of X ;
take x ; :: thesis: S₁[n,x]
thus S₁[n,x] by A2; :: thesis: verum

end;

suppose A3: n = i ; :: thesis: ex x being Element of X st S₁[n,x]

reconsider x = f . j as Element of X ;
take x ; :: thesis: S₁[n,x]
thus S₁[n,x] by A3; :: thesis: verum

end;

suppose A4: n = j ; :: thesis: ex x being Element of X st S₁[n,x]

reconsider x = f . i as Element of X ;
take x ; :: thesis: S₁[n,x]
thus S₁[n,x] by A4; :: thesis: verum

end;

end;

end;

consider g being Function of NAT,X such that
A5: for n being Element of NAT holds S₁[n,g . n] from FUNCT_2:sch 3(A1);
take g ; :: thesis: ( ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i )
A6: ( i is Element of NAT & j is Element of NAT ) by ORDINAL1:def 12;

hereby :: thesis: ( f . i = g . j & f . j = g . i )

let n be Nat; :: thesis: ( n <> i & n <> j implies f . n = g . n )
assume A7: ( n <> i & n <> j ) ; :: thesis: f . n = g . n
n is Element of NAT by ORDINAL1:def 12;
hence f . n = g . n by A5, A7; :: thesis: verum

end;

thus ( f . i = g . j & f . j = g . i ) by A5, A6; :: thesis: verum