let X, Y be finite natural-membered set ; :: thesis: ( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )
set p = Sgm0 X;
set q = Sgm0 Y;
set r = Sgm0 (X \/ Y);
thus ( X <N< Y implies Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) ) :: thesis: ( Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) implies X <N< Y )

proof

defpred S₁[ Nat] means ( $1 in dom (Sgm0 X) implies (Sgm0 (X \/ Y)) . $1 = (Sgm0 X) . $1 );
reconsider X1 = X, Y1 = Y as finite set ;
assume A1: X <N< Y ; :: thesis: Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
X /\ Y = {}

proof

set x = the Element of X /\ Y;
A2: X = rng (Sgm0 X) by Def4;
assume A3: not X /\ Y = {} ; :: thesis: contradiction
then the Element of X /\ Y in X by XBOOLE_0:def 4;
then reconsider m = the Element of X /\ Y as Element of NAT by A2;
A4: m in Y by A3, XBOOLE_0:def 4;
m in X by A3, XBOOLE_0:def 4;
hence contradiction by A1, A4; :: thesis: verum

end;

then A5: X misses Y ;
A6: len (Sgm0 (X \/ Y)) = card (X1 \/ Y1) by Th20
.= (card X1) + (card Y1) by A5, CARD_2:40
.= (len (Sgm0 X)) + (card Y1) by Th20
.= (len (Sgm0 X)) + (len (Sgm0 Y)) by Th20 ;

A7: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

set m = (Sgm0 (X \/ Y)) . (k + 1);
set n = (Sgm0 X) . (k + 1);
assume A9: k + 1 in dom (Sgm0 X) ; :: thesis: (Sgm0 (X \/ Y)) . (k + 1) = (Sgm0 X) . (k + 1)
then (Sgm0 X) . (k + 1) in rng (Sgm0 X) by FUNCT_1:def 3;
then A10: (Sgm0 X) . (k + 1) in X by Def4;
len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by A6, NAT_1:12;
then A11: Segm (len (Sgm0 X)) c= Segm (len (Sgm0 (X \/ Y))) by NAT_1:39;
then (Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 (X \/ Y)) by A9, FUNCT_1:def 3;
then A12: (Sgm0 (X \/ Y)) . (k + 1) in X \/ Y by Def4;
assume A13: (Sgm0 (X \/ Y)) . (k + 1) <> (Sgm0 X) . (k + 1) ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( k in dom (Sgm0 X) or not k in dom (Sgm0 X) ) ;

suppose A14: k in dom (Sgm0 X) ; :: thesis: contradiction

set m1 = (Sgm0 (X \/ Y)) . k;
set n1 = (Sgm0 X) . k;

now :: thesis: contradiction

per cases ( (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) or (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ) by A13, XXREAL_0:1;

suppose A15: (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) ; :: thesis: contradiction

then not (Sgm0 (X \/ Y)) . (k + 1) in Y by A1, A10;
then (Sgm0 (X \/ Y)) . (k + 1) in X by A12, XBOOLE_0:def 3;
then (Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 X) by Def4;
then consider x being object such that
A16: x in dom (Sgm0 X) and
A17: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . (k + 1) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A16;
x < len (Sgm0 X) by A16, AFINSQ_1:86;
then A18: x < k + 1 by A15, A17, Th33;
A19: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 (X \/ Y)) by A9, A11, AFINSQ_1:86;
then A20: (Sgm0 X) . k < (Sgm0 (X \/ Y)) . (k + 1) by A8, A14, A19, Def4;
k < len (Sgm0 X) by A14, AFINSQ_1:86;
then k < x by A17, A20, Th33;
hence contradiction by A18, NAT_1:13; :: thesis: verum

end;

suppose A21: (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ; :: thesis: contradiction

(Sgm0 X) . (k + 1) in X \/ Y by A10, XBOOLE_0:def 3;
then (Sgm0 X) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4;
then consider x being object such that
A22: x in dom (Sgm0 (X \/ Y)) and
A23: (Sgm0 (X \/ Y)) . x = (Sgm0 X) . (k + 1) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A22;
x < len (Sgm0 (X \/ Y)) by A22, AFINSQ_1:86;
then A24: x < k + 1 by A21, A23, Th33;
A25: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 X) by A9, AFINSQ_1:86;
then A26: (Sgm0 (X \/ Y)) . k < (Sgm0 X) . (k + 1) by A8, A14, A25, Def4;
k < len (Sgm0 (X \/ Y)) by A11, A14, AFINSQ_1:86;
then k < x by A23, A26, Th33;
hence contradiction by A24, NAT_1:13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A27: not k in dom (Sgm0 X) ; :: thesis: contradiction

A28: k < k + 1 by XREAL_1:29;
len (Sgm0 X) <= k by A27, AFINSQ_1:86;
then len (Sgm0 X) < k + 1 by A28, XXREAL_0:2;
hence contradiction by A9, AFINSQ_1:86; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

( 0 < len (Sgm0 X) implies X1 <> {} ) by Th20, CARD_1:27;
then A29: S₁[ 0 ] by A1, Th34;
A30: for k being Nat holds S₁[k] from NAT_1:sch 2(A29, A7);
defpred S₂[ Nat] means ( $1 in dom (Sgm0 Y) implies (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + $1) = (Sgm0 Y) . $1 );

A31: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A32: S₂[k] ; :: thesis: S₂[k + 1]
thus S₂[k + 1] :: thesis: verum

proof

set n = (Sgm0 Y) . (k + 1);
set a = (len (Sgm0 X)) + (k + 1);
set m = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1));
assume A33: k + 1 in dom (Sgm0 Y) ; :: thesis: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) = (Sgm0 Y) . (k + 1)
then (Sgm0 Y) . (k + 1) in rng (Sgm0 Y) by FUNCT_1:def 3;
then A34: (Sgm0 Y) . (k + 1) in Y by Def4;
k + 1 < len (Sgm0 Y) by A33, AFINSQ_1:86;
then A35: (len (Sgm0 X)) + (k + 1) < len (Sgm0 (X \/ Y)) by A6, XREAL_1:6;
then A36: (len (Sgm0 X)) + (k + 1) in dom (Sgm0 (X \/ Y)) by AFINSQ_1:86;
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 (X \/ Y)) by FUNCT_1:def 3;
then A37: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X \/ Y by Def4;

A38: now :: thesis: not (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X

A39: len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by A6, NAT_1:12;
assume (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X ; :: thesis: contradiction
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 X) by Def4;
then consider x being object such that
A40: x in dom (Sgm0 X) and
A41: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A40;
x < len (Sgm0 X) by A40, AFINSQ_1:86;
then x < len (Sgm0 (X \/ Y)) by A39, XXREAL_0:2;
then A42: x in dom (Sgm0 (X \/ Y)) by AFINSQ_1:86;
(Sgm0 (X \/ Y)) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A30, A40, A41;
then x = (len (Sgm0 X)) + (k + 1) by A36, A42, FUNCT_1:def 4;
then (len (Sgm0 X)) + (k + 1) <= (len (Sgm0 X)) + 0 by A40, AFINSQ_1:86;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

assume A43: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) <> (Sgm0 Y) . (k + 1) ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( k in dom (Sgm0 Y) or not k in dom (Sgm0 Y) ) ;

suppose A44: k in dom (Sgm0 Y) ; :: thesis: contradiction

set m1 = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k);
set n1 = (Sgm0 Y) . k;
A45: k < len (Sgm0 Y) by A44, AFINSQ_1:86;

now :: thesis: contradiction

per cases ( (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) or (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ) by A43, XXREAL_0:1;

suppose A46: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) ; :: thesis: contradiction

(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in Y by A37, A38, XBOOLE_0:def 3;
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 Y) by Def4;
then consider x being object such that
A47: x in dom (Sgm0 Y) and
A48: (Sgm0 Y) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A47;
x < len (Sgm0 Y) by A47, AFINSQ_1:86;
then A49: x < k + 1 by A46, A48, Th33;
(len (Sgm0 X)) + k < ((len (Sgm0 X)) + k) + 1 by XREAL_1:29;
then A50: (Sgm0 Y) . k < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A32, A35, A44, Def4;
k < len (Sgm0 Y) by A44, AFINSQ_1:86;
then k < x by A48, A50, Th33;
hence contradiction by A49, NAT_1:13; :: thesis: verum

end;

suppose A51: (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ; :: thesis: contradiction

(Sgm0 Y) . (k + 1) in X \/ Y by A34, XBOOLE_0:def 3;
then (Sgm0 Y) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4;
then consider x being object such that
A52: x in dom (Sgm0 (X \/ Y)) and
A53: (Sgm0 (X \/ Y)) . x = (Sgm0 Y) . (k + 1) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A52;
x < len (Sgm0 (X \/ Y)) by A52, AFINSQ_1:86;
then A54: x < ((len (Sgm0 X)) + k) + 1 by A51, A53, Th33;
A55: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 Y) by A33, AFINSQ_1:86;
then A56: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k) < (Sgm0 Y) . (k + 1) by A32, A44, A55, Def4;
(len (Sgm0 X)) + k < len (Sgm0 (X \/ Y)) by A6, A45, XREAL_1:6;
then (len (Sgm0 X)) + k < x by A53, A56, Th33;
hence contradiction by A54, NAT_1:13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A57: not k in dom (Sgm0 Y) ; :: thesis: contradiction

A58: k < k + 1 by XREAL_1:29;
len (Sgm0 Y) <= k by A57, AFINSQ_1:86;
hence contradiction by A33, AFINSQ_1:86, A58, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

( len (Sgm0 Y) > 0 implies Y <> {} ) by Th20, CARD_1:27;
then A59: S₂[ 0 ] by A1, Th32;
for k being Nat holds S₂[k] from NAT_1:sch 2(A59, A31);
hence Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) by A6, A30, AFINSQ_1:def 3; :: thesis: verum

end;

assume A60: Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) ; :: thesis: X <N< Y
let m, n be Nat; :: according to AFINSQ_2:def 5 :: thesis: ( m in X & n in Y implies m < n )
assume that
A61: m in X and
A62: n in Y ; :: thesis: m < n
n in rng (Sgm0 Y) by A62, Def4;
then consider y being object such that
A63: y in dom (Sgm0 Y) and
A64: (Sgm0 Y) . y = n by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A63;
A65: n = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + y) by A60, A63, A64, AFINSQ_1:def 3;
y < len (Sgm0 Y) by A63, AFINSQ_1:86;
then (len (Sgm0 X)) + y < (len (Sgm0 X)) + (len (Sgm0 Y)) by XREAL_1:6;
then A66: (len (Sgm0 X)) + y < len (Sgm0 (X \/ Y)) by A60, AFINSQ_1:17;
A67: len (Sgm0 X) <= (len (Sgm0 X)) + y by NAT_1:12;
m in rng (Sgm0 X) by A61, Def4;
then consider x being object such that
A68: x in dom (Sgm0 X) and
A69: (Sgm0 X) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A68;
x < len (Sgm0 X) by A68, AFINSQ_1:86;
then A70: x < (len (Sgm0 X)) + y by A67, XXREAL_0:2;
m = (Sgm0 (X \/ Y)) . x by A60, A68, A69, AFINSQ_1:def 3;
hence m < n by A65, A70, A66, Def4; :: thesis: verum