let X be non empty set ; 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; 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; 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 S1[ 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 S1[n,x]
proof
let n be
Element of
NAT ;
ex x being Element of X st S1[n,x]
per cases
( ( n <> i & n <> j ) or n = i or n = j )
;
suppose A2:
(
n <> i &
n <> j )
;
ex x being Element of X st S1[n,x]reconsider x =
f . n as
Element of
X ;
take
x
;
S1[n,x]thus
S1[
n,
x]
by A2;
verum end; suppose A3:
n = i
;
ex x being Element of X st S1[n,x]reconsider x =
f . j as
Element of
X ;
take
x
;
S1[n,x]thus
S1[
n,
x]
by A3;
verum end; suppose A4:
n = j
;
ex x being Element of X st S1[n,x]reconsider x =
f . i as
Element of
X ;
take
x
;
S1[n,x]thus
S1[
n,
x]
by A4;
verum end;
end;
consider g being Function of NAT,X such that
A5:
for n being Element of NAT holds S1[n,g . n]
from FUNCT_2:sch 3(A1);
take
g
; ( ( 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 ( f . i = g . j & f . j = g . i )
end;
thus
( f . i = g . j & f . j = g . i )
by A5, A6; verum