let X be set ; for A being finite Subset of X
for R being Order of X
for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds
f = SgmX (R,A)
let A be finite Subset of X; for R being Order of X
for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds
f = SgmX (R,A)
let R be Order of X; for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds
f = SgmX (R,A)
let f be FinSequence of X; ( rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) implies f = SgmX (R,A) )
assume that
A1:
rng f = A
and
A2:
for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R )
; f = SgmX (R,A)
now for a, b being object st a in A & b in A & a <> b & not [a,b] in R holds
[b,a] in Rlet a,
b be
object ;
( a in A & b in A & a <> b & not [a,b] in R implies [b,a] in R )assume that A3:
a in A
and A4:
b in A
and A5:
a <> b
;
( [a,b] in R or [b,a] in R )consider n being
Nat such that A6:
n in dom f
and A7:
f . n = a
by A1, A3, FINSEQ_2:10;
consider m being
Nat such that A8:
m in dom f
and A9:
f . m = b
by A1, A4, FINSEQ_2:10;
A10:
f /. m = f . m
by A8, PARTFUN1:def 6;
A11:
f /. n = f . n
by A6, PARTFUN1:def 6;
now ( not [a,b] in R implies [b,a] in R )assume that A12:
not
[a,b] in R
and A13:
not
[b,a] in R
;
contradictionper cases
( n = m or n <> m )
;
suppose
n = m
;
contradictionhence
contradiction
by A5, A7, A9;
verum end; suppose A14:
n <> m
;
contradictionhence
contradiction
;
verum end; end; end; hence
(
[a,b] in R or
[b,a] in R )
;
verum end;
then A15:
R is_connected_in A
;
A16:
field R = X
by ORDERS_1:12;
then A17:
R is_antisymmetric_in A
by ORDERS_1:9, RELAT_2:def 12;
R is_transitive_in X
by A16, RELAT_2:def 16;
then A18:
R is_transitive_in A
;
R is_reflexive_in X
by A16, RELAT_2:def 9;
then
R is_reflexive_in A
;
then
R linearly_orders A
by A17, A18, A15, ORDERS_1:def 9;
hence
f = SgmX (R,A)
by A1, A2, Def2; verum