let i be Nat; :: thesis: for X0, Y0 being finite natural-membered set st X0 <N< Y0 & i < card Y0 holds
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
let X0, Y0 be finite natural-membered set ; :: thesis: ( X0 <N< Y0 & i < card Y0 implies ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) )
assume that
A1: X0 <N< Y0 and
A2: i < card Y0 ; :: thesis: ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
consider n being Nat such that
A3: Y0 c= Segm n by Th2;
X0 /\ Y0 = X0 /\ (Y0 /\ NAT) by A3, XBOOLE_1:1, XBOOLE_1:28
.= (X0 /\ Y0) /\ NAT by XBOOLE_1:16
.= {} by A1, Th23 ;
then A4: X0 misses Y0 ;
set f = (Sgm0 (X0 \/ Y0)) /^ (card X0);
set f0 = Sgm0 (X0 \/ Y0);
set Z = { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ;
A5: dom ((Sgm0 (X0 \/ Y0)) /^ (card X0)),((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) are_equipotent by CARD_1:33;
A6: rng (Sgm0 (X0 \/ Y0)) = X0 \/ Y0 by Def4;
A7: len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th20;
then A8: card X0 <= len (Sgm0 (X0 \/ Y0)) by NAT_1:43, XBOOLE_1:7;
A9: len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = (len (Sgm0 (X0 \/ Y0))) -' (card X0) by Def2
.= (len (Sgm0 (X0 \/ Y0))) - (card X0) by A8, XREAL_1:233 ;
A10: (X0 \/ Y0) \ X0 = (X0 \ X0) \/ (Y0 \ X0) by XBOOLE_1:42
.= {} \/ (Y0 \ X0) by XBOOLE_1:37
.= Y0 by A4, XBOOLE_1:83 ;
then A11: len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = card Y0 by A7, A9, CARD_2:44, XBOOLE_1:7;
A12: { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= rng ((Sgm0 (X0 \/ Y0)) /^ (card X0))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } or y in rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) )
assume y in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ; :: thesis: y in rng ((Sgm0 (X0 \/ Y0)) /^ (card X0))
then ex v0 being Element of X0 \/ Y0 st
( y = v0 & ex k2 being Nat st
( v0 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) ) ;
hence y in rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) by A11, FUNCT_1:def 3; :: thesis: verum
end;
then reconsider Z0 = { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } as finite set ;
A13: ((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) = rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) by RELAT_1:113;
A14: rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) c= rng (Sgm0 (X0 \/ Y0)) by Th9;
A15: rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) or y in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } )
assume A16: y in rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) ; :: thesis: y in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) }
then consider x being object such that
A17: x in dom ((Sgm0 (X0 \/ Y0)) /^ (card X0)) and
A18: y = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . x by FUNCT_1:def 3;
reconsider y0 = y as Element of X0 \/ Y0 by A14, A16, Def4;
ex k2 being Nat st
( y0 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) by A11, A17, A18;
hence y in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ; :: thesis: verum
end;
then rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } by A12;
then card { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } = card (len ((Sgm0 (X0 \/ Y0)) /^ (card X0))) by A5, A13, CARD_1:5;
then A19: card { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } = card Y0 by A7, A9, A10, CARD_2:44, XBOOLE_1:7;
len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th20;
then A20: len (Sgm0 (X0 \/ Y0)) = (card X0) + (card Y0) by A4, CARD_2:40;
A21: X0 \/ Y0 <> {} by A2, CARD_1:27, XBOOLE_1:15;
A22: now :: thesis: ( not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= Y0 implies Y0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } )
assume that
A23: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= Y0 and
A24: not Y0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ; :: thesis: contradiction
consider v2 being object such that
A25: v2 in Y0 and
A26: not v2 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } by A24;
Y0 c= X0 \/ Y0 by XBOOLE_1:7;
then consider x2 being object such that
A27: x2 in dom (Sgm0 (X0 \/ Y0)) and
A28: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A6, A25, FUNCT_1:def 3;
consider v1 being object such that
A29: v1 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } and
A30: not v1 in Y0 by A23;
consider v10 being Element of X0 \/ Y0 such that
A31: v1 = v10 and
A32: ex k2 being Nat st
( v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in Segm (card Y0) ) by A29;
A33: v10 in X0 by A21, A30, A31, XBOOLE_0:def 3;
reconsider nv10 = v10 as Nat ;
reconsider nv2 = v2 as Nat by A28;
consider k20 being Nat such that
A34: v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 and
A35: k20 in Segm (card Y0) by A32;
A36: k20 + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, XREAL_1:6, A35, NAT_1:44;
then A37: ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . (k20 + (card X0)) by Th8;
reconsider x20 = x2 as Nat by A27;
set nx20 = x20 -' (card X0);
A38: v2 in X0 \/ Y0 by A6, A27, A28, FUNCT_1:def 3;
A39: now :: thesis: not x20 >= card X0
assume A40: x20 >= card X0 ; :: thesis: contradiction
then A41: x20 -' (card X0) = x20 - (card X0) by XREAL_1:233;
x20 < (card X0) + (card Y0) by A20, A27, AFINSQ_1:86;
then x20 - (card X0) < ((card X0) + (card Y0)) - (card X0) by XREAL_1:9;
then A42: x20 -' (card X0) < card Y0 by A40, XREAL_1:233;
then A43: x20 -' (card X0) in Segm (card Y0) by NAT_1:44;
(x20 -' (card X0)) + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, A42, XREAL_1:6;
then ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . (x20 -' (card X0)) = (Sgm0 (X0 \/ Y0)) . x20 by A41, Th8;
hence contradiction by A26, A28, A38, A43; :: thesis: verum
end;
card X0 <= (card X0) + k20 by NAT_1:12;
then k20 + (card X0) > x20 by A39, XXREAL_0:2;
then nv10 > nv2 by A34, A28, A36, A37, Def4;
hence contradiction by A1, A25, A33; :: thesis: verum
end;
A44: now :: thesis: ( ( Z0 c= Y0 & Z0 = Y0 ) or ( Y0 c= Z0 & Z0 = Y0 ) )
per cases ( Z0 c= Y0 or Y0 c= Z0 ) by A22;
case Z0 c= Y0 ; :: thesis: Z0 = Y0
hence Z0 = Y0 by A19, CARD_2:102; :: thesis: verum
end;
case Y0 c= Z0 ; :: thesis: Z0 = Y0
hence Z0 = Y0 by A19, CARD_2:102; :: thesis: verum
end;
end;
end;
i + (card X0) < len (Sgm0 (X0 \/ Y0)) by A2, A9, A11, XREAL_1:20;
hence ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) by A15, A12, A44, Th8; :: thesis: verum