:: PENCIL_2 semantic presentation begin definition let D be set ; let p be FinSequence of D; let i, j be Nat; func Del (p,i,j) -> FinSequence of D equals :: PENCIL_2:def 1 (p | (i -' 1)) ^ (p /^ j); coherence (p | (i -' 1)) ^ (p /^ j) is FinSequence of D ; end; :: deftheorem defines Del PENCIL_2:def_1_:_ for D being set for p being FinSequence of D for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j); theorem Th1: :: PENCIL_2:1 for D being set for p being FinSequence of D for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p proof let D be set ; ::_thesis: for p being FinSequence of D for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p let p be FinSequence of D; ::_thesis: for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p let i, j be Element of NAT ; ::_thesis: rng (Del (p,i,j)) c= rng p A1: rng (p /^ j) c= rng p proof percases ( D is empty or not D is empty ) ; supposeA2: D is empty ; ::_thesis: rng (p /^ j) c= rng p then A3: ( j > len p implies rng (p /^ j) c= rng p ) ; ( j <= len p implies rng (p /^ j) c= rng p ) by A2; hence rng (p /^ j) c= rng p by A3; ::_thesis: verum end; suppose not D is empty ; ::_thesis: rng (p /^ j) c= rng p then reconsider E = D as non empty set ; reconsider r = p as FinSequence of E ; rng (r /^ j) c= rng r by FINSEQ_5:33; hence rng (p /^ j) c= rng p ; ::_thesis: verum end; end; end; rng (p | (i -' 1)) = rng (p | (Seg (i -' 1))) by FINSEQ_1:def_15; then A4: rng (p | (i -' 1)) c= rng p by RELAT_1:70; rng ((p | (i -' 1)) ^ (p /^ j)) = (rng (p | (i -' 1))) \/ (rng (p /^ j)) by FINSEQ_1:31; hence rng (Del (p,i,j)) c= rng p by A4, A1, XBOOLE_1:8; ::_thesis: verum end; theorem Th2: :: PENCIL_2:2 for D being set for p being FinSequence of D for i, j being Element of NAT st i in dom p & j in dom p holds len (Del (p,i,j)) = (((len p) - j) + i) - 1 proof let D be set ; ::_thesis: for p being FinSequence of D for i, j being Element of NAT st i in dom p & j in dom p holds len (Del (p,i,j)) = (((len p) - j) + i) - 1 let p be FinSequence of D; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p holds len (Del (p,i,j)) = (((len p) - j) + i) - 1 let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p implies len (Del (p,i,j)) = (((len p) - j) + i) - 1 ) assume that A1: i in dom p and A2: j in dom p ; ::_thesis: len (Del (p,i,j)) = (((len p) - j) + i) - 1 A3: i <= len p by A1, FINSEQ_3:25; 1 <= i by A1, FINSEQ_3:25; then A4: i - 1 >= 1 - 1 by XREAL_1:9; A5: i -' 1 <= i by NAT_D:35; A6: j <= len p by A2, FINSEQ_3:25; thus len (Del (p,i,j)) = (len (p | (i -' 1))) + (len (p /^ j)) by FINSEQ_1:22 .= (i -' 1) + (len (p /^ j)) by A3, A5, FINSEQ_1:59, XXREAL_0:2 .= (i -' 1) + ((len p) - j) by A6, RFINSEQ:def_1 .= (i - 1) + ((len p) - j) by A4, XREAL_0:def_2 .= (((len p) - j) + i) - 1 ; ::_thesis: verum end; theorem Th3: :: PENCIL_2:3 for D being set for p being FinSequence of D for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds ( i = 1 & j = len p ) proof let D be set ; ::_thesis: for p being FinSequence of D for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds ( i = 1 & j = len p ) let p be FinSequence of D; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds ( i = 1 & j = len p ) let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & len (Del (p,i,j)) = 0 implies ( i = 1 & j = len p ) ) assume that A1: i in dom p and A2: j in dom p and A3: len (Del (p,i,j)) = 0 ; ::_thesis: ( i = 1 & j = len p ) A4: 1 <= i by A1, FINSEQ_3:25; j <= len p by A2, FINSEQ_3:25; then A5: (len p) - j >= 0 by XREAL_1:48; A6: (((len p) - j) + i) - 1 = 0 by A1, A2, A3, Th2; then (len p) - j = 1 - i ; then 1 >= i by A5, XREAL_1:49; hence i = 1 by A4, XXREAL_0:1; ::_thesis: j = len p hence j = len p by A6; ::_thesis: verum end; theorem Th4: :: PENCIL_2:4 for D being set for p being FinSequence of D for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds (Del (p,i,j)) . k = p . k proof let D be set ; ::_thesis: for p being FinSequence of D for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds (Del (p,i,j)) . k = p . k let p be FinSequence of D; ::_thesis: for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds (Del (p,i,j)) . k = p . k let i, j, k be Element of NAT ; ::_thesis: ( i in dom p & 1 <= k & k <= i - 1 implies (Del (p,i,j)) . k = p . k ) assume that A1: i in dom p and A2: 1 <= k and A3: k <= i - 1 ; ::_thesis: (Del (p,i,j)) . k = p . k A4: i <= len p by A1, FINSEQ_3:25; A5: k <= i -' 1 by A3, XREAL_0:def_2; A6: i -' 1 <= i by NAT_D:35; then len (p | (i -' 1)) = i -' 1 by A4, FINSEQ_1:59, XXREAL_0:2; then A7: k in dom (p | (i -' 1)) by A2, A5, FINSEQ_3:25; i -' 1 <= len p by A4, A6, XXREAL_0:2; then k <= len p by A5, XXREAL_0:2; then A8: k in dom p by A2, FINSEQ_3:25; thus (Del (p,i,j)) . k = (p | (i -' 1)) . k by A7, FINSEQ_1:def_7 .= (p | (i -' 1)) /. k by A7, PARTFUN1:def_6 .= p /. k by A7, FINSEQ_4:70 .= p . k by A8, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th5: :: PENCIL_2:5 for p, q being FinSequence for k being Element of NAT st (len p) + 1 <= k holds (p ^ q) . k = q . (k - (len p)) proof let p, q be FinSequence; ::_thesis: for k being Element of NAT st (len p) + 1 <= k holds (p ^ q) . k = q . (k - (len p)) let k be Element of NAT ; ::_thesis: ( (len p) + 1 <= k implies (p ^ q) . k = q . (k - (len p)) ) assume A1: (len p) + 1 <= k ; ::_thesis: (p ^ q) . k = q . (k - (len p)) percases ( k <= (len p) + (len q) or not k <= (len p) + (len q) ) ; suppose k <= (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p)) hence (p ^ q) . k = q . (k - (len p)) by A1, FINSEQ_1:23; ::_thesis: verum end; supposeA2: not k <= (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p)) then k - (len p) > len q by XREAL_1:20; then A3: not k - (len p) in dom q by FINSEQ_3:25; not k <= len (p ^ q) by A2, FINSEQ_1:22; then not k in dom (p ^ q) by FINSEQ_3:25; hence (p ^ q) . k = {} by FUNCT_1:def_2 .= q . (k - (len p)) by A3, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; theorem Th6: :: PENCIL_2:6 for D being set for p being FinSequence of D for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) proof let D be set ; ::_thesis: for p being FinSequence of D for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) let p be FinSequence of D; ::_thesis: for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) let i, j, k be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 implies (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) ) assume that A1: i in dom p and A2: j in dom p and A3: i <= j and A4: i <= k and A5: k <= (((len p) - j) + i) - 1 ; ::_thesis: (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) A6: i -' 1 <= i by NAT_D:35; i -' 1 <= i by NAT_D:35; then k >= i -' 1 by A4, XXREAL_0:2; then k - (i -' 1) >= (i -' 1) - (i -' 1) by XREAL_1:9; then A7: k - (i -' 1) = k -' (i -' 1) by XREAL_0:def_2; A8: 1 <= i by A1, FINSEQ_3:25; then A9: (i -' 1) + 1 <= k by A4, XREAL_1:235; i - 1 >= 1 - 1 by A8, XREAL_1:9; then A10: i -' 1 = i - 1 by XREAL_0:def_2; j - i >= i - i by A3, XREAL_1:9; then A11: j -' i = j - i by XREAL_0:def_2; A12: j <= len p by A2, FINSEQ_3:25; then A13: len (p /^ j) = (len p) - j by RFINSEQ:def_1; k <= ((len p) - j) + (i - 1) by A5; then A14: k - (i -' 1) <= (len p) - j by A10, XREAL_1:20; 1 <= k - (i -' 1) by A9, XREAL_1:19; then A15: k - (i -' 1) in dom (p /^ j) by A7, A13, A14, FINSEQ_3:25; i <= len p by A1, FINSEQ_3:25; then len (p | (i -' 1)) = i -' 1 by A6, FINSEQ_1:59, XXREAL_0:2; hence (Del (p,i,j)) . k = (p /^ j) . (k - (i -' 1)) by A9, Th5 .= p . (j + (k + (1 - i))) by A12, A10, A15, RFINSEQ:def_1 .= p . (((j -' i) + k) + 1) by A11 ; ::_thesis: verum end; scheme :: PENCIL_2:sch 1 FinSeqOneToOne{ F1() -> set , F2() -> set , F3() -> set , F4() -> FinSequence of F3(), P1[ set , set ] } : ex g being one-to-one FinSequence of F3() st ( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds P1[g . j,g . (j + 1)] ) ) provided A1: ( F1() = F4() . 1 & F2() = F4() . (len F4()) ) and A2: for i being Element of NAT for d1, d2 being set st 1 <= i & i < len F4() & d1 = F4() . i & d2 = F4() . (i + 1) holds P1[d1,d2] proof defpred S1[ Nat] means ex f being FinSequence of F3() st ( len f = $1 & F1() = f . 1 & F2() = f . (len f) & rng f c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len f holds P1[f . i,f . (i + 1)] ) ); for i being Element of NAT st 1 <= i & i < len F4() holds P1[F4() . i,F4() . (i + 1)] by A2; then A3: ex k being Nat st S1[k] by A1; consider k being Nat such that A4: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A3); consider g being FinSequence of F3() such that A5: len g = k and A6: F1() = g . 1 and A7: F2() = g . (len g) and A8: rng g c= rng F4() and A9: for i being Element of NAT st 1 <= i & i < len g holds P1[g . i,g . (i + 1)] by A4; now__::_thesis:_g_is_one-to-one assume not g is one-to-one ; ::_thesis: contradiction then consider x, y being set such that A10: x in dom g and A11: y in dom g and A12: g . x = g . y and A13: x <> y by FUNCT_1:def_4; reconsider x = x, y = y as Element of NAT by A10, A11; percases ( x < y or y < x ) by A13, XXREAL_0:1; supposeA14: x < y ; ::_thesis: contradiction set d = Del (g,(x + 1),y); A15: 1 <= y by A11, FINSEQ_3:25; A16: x + 1 >= 1 by NAT_1:11; A17: y <= len g by A11, FINSEQ_3:25; then A18: x < len g by A14, XXREAL_0:2; then x + 1 <= len g by NAT_1:13; then A19: x + 1 in dom g by A16, FINSEQ_3:25; A20: x + 1 <= y by A14, NAT_1:13; then A21: y - (x + 1) >= 0 by XREAL_1:48; A22: ( rng (Del (g,(x + 1),y)) c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] ) ) proof rng (Del (g,(x + 1),y)) c= rng g by Th1; hence rng (Del (g,(x + 1),y)) c= rng F4() by A8, XBOOLE_1:1; ::_thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (Del (g,(x + 1),y)) implies P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] ) assume that A23: 1 <= i and A24: i < len (Del (g,(x + 1),y)) ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] percases ( i < x or i = x or i > x ) by XXREAL_0:1; supposeA25: i < x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] then i + 1 <= (x + 1) - 1 by NAT_1:13; then A26: (Del (g,(x + 1),y)) . (i + 1) = g . (i + 1) by A19, Th4, NAT_1:11; i <= (x + 1) - 1 by A25; then A27: (Del (g,(x + 1),y)) . i = g . i by A19, A23, Th4; i < len g by A18, A25, XXREAL_0:2; hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A23, A27, A26; ::_thesis: verum end; supposeA28: i = x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] now__::_thesis:_not_y_=_len_g assume y = len g ; ::_thesis: contradiction then x < (((len g) - (len g)) + (x + 1)) - 1 by A11, A19, A24, A28, Th2; hence contradiction ; ::_thesis: verum end; then A29: y < len g by A17, XXREAL_0:1; then A30: 0 < (len g) - y by XREAL_1:50; then 0 < (len g) -' y by XREAL_0:def_2; then 0 + 1 <= (len g) -' y by NAT_1:13; then 1 - 1 <= ((len g) -' y) - 1 by XREAL_1:9; then 0 <= ((len g) - y) - 1 by A30, XREAL_0:def_2; then (i + 1) + 0 <= (i + 1) + (((len g) - y) - 1) by XREAL_1:7; then (i + 1) + 0 <= ((i + 1) + ((len g) - y)) - 1 ; then A31: (Del (g,(x + 1),y)) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A11, A20, A19, A28, Th6 .= g . (y + 1) by A20, A28, XREAL_1:235 ; i <= (x + 1) - 1 by A28; then (Del (g,(x + 1),y)) . i = g . y by A12, A19, A23, A28, Th4; hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A15, A29, A31; ::_thesis: verum end; suppose i > x ; ::_thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] then A32: x + 1 <= i by NAT_1:13; A33: (len g) - y >= 0 by A17, XREAL_1:48; i < (((len g) - y) + (x + 1)) - 1 by A11, A19, A24, Th2; then A34: i < (((len g) -' y) + (x + 1)) - 1 by A33, XREAL_0:def_2; then i + 1 <= ((len g) -' y) + x by NAT_1:13; then i + 1 <= ((((len g) - y) + x) + 1) - 1 by A33, XREAL_0:def_2; then A35: i + 1 <= (((len g) - y) + (x + 1)) - 1 ; i < ((((len g) -' y) + x) + 1) - 1 by A34; then i < ((len g) - y) + x by A33, XREAL_0:def_2; then i - x < (((len g) - y) + x) - x by XREAL_1:9; then (i - x) + y < ((len g) - y) + y by XREAL_1:8; then (((y - x) - 1) + i) + 1 < len g ; then A36: ((y -' (x + 1)) + i) + 1 < len g by A21, XREAL_0:def_2; i <= i + 1 by NAT_1:11; then x + 1 <= i + 1 by A32, XXREAL_0:2; then A37: (Del (g,(x + 1),y)) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A11, A20, A19, A35, Th6 .= g . ((((y -' (x + 1)) + i) + 1) + 1) ; i <= (((len g) - y) + (x + 1)) - 1 by A11, A19, A24, Th2; then (Del (g,(x + 1),y)) . i = g . (((y -' (x + 1)) + i) + 1) by A11, A20, A19, A32, Th6; hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A37, A36, NAT_1:11; ::_thesis: verum end; end; end; A38: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) proof percases ( len (Del (g,(x + 1),y)) <= x or len (Del (g,(x + 1),y)) > x ) ; supposeA39: len (Del (g,(x + 1),y)) <= x ; ::_thesis: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) now__::_thesis:_not_len_(Del_(g,(x_+_1),y))_=_0 assume len (Del (g,(x + 1),y)) = 0 ; ::_thesis: contradiction then x + 1 = 0 + 1 by A11, A19, Th3; hence contradiction by A10, FINSEQ_3:24; ::_thesis: verum end; then A40: 0 + 1 <= len (Del (g,(x + 1),y)) by NAT_1:13; len (Del (g,(x + 1),y)) <= (x + 1) - 1 by A39; then A41: (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) = g . (len (Del (g,(x + 1),y))) by A19, A40, Th4; (((len g) - y) + (x + 1)) - 1 <= x by A11, A19, A39, Th2; then ((((len g) - y) + x) + 1) - 1 <= x ; then (len g) - y <= 0 by XREAL_1:29; then len g <= y by XREAL_1:50; then A42: len g = y by A17, XXREAL_0:1; then x <= (((len g) - y) + (x + 1)) - 1 ; hence F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) by A7, A11, A12, A19, A42, A41, Th2; ::_thesis: verum end; suppose len (Del (g,(x + 1),y)) > x ; ::_thesis: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) then A43: x + 1 <= len (Del (g,(x + 1),y)) by NAT_1:13; len (Del (g,(x + 1),y)) = (((len g) - y) + (x + 1)) - 1 by A11, A19, Th2; hence (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) = g . (((y -' (x + 1)) + ((((len g) - y) + (x + 1)) - 1)) + 1) by A11, A20, A19, A43, Th6 .= g . (((y - (x + 1)) + ((x + 1) + (((len g) - y) - 1))) + 1) by A20, XREAL_1:233 .= F2() by A7 ; ::_thesis: verum end; end; end; 1 <= (x + 1) - 1 by A10, FINSEQ_3:25; then A44: F1() = (Del (g,(x + 1),y)) . 1 by A6, A19, Th4; 0 < - (- (y - x)) by A14, XREAL_1:50; then - (y - x) < 0 ; then (len g) + (- (y - x)) < (len g) + 0 by XREAL_1:8; then (((len g) - y) + (x + 1)) - 1 < len g ; then len (Del (g,(x + 1),y)) < len g by A11, A19, Th2; hence contradiction by A4, A5, A44, A38, A22; ::_thesis: verum end; supposeA45: y < x ; ::_thesis: contradiction set d = Del (g,(y + 1),x); A46: 1 <= x by A10, FINSEQ_3:25; A47: y + 1 >= 1 by NAT_1:11; A48: x <= len g by A10, FINSEQ_3:25; then A49: y < len g by A45, XXREAL_0:2; then y + 1 <= len g by NAT_1:13; then A50: y + 1 in dom g by A47, FINSEQ_3:25; A51: y + 1 <= x by A45, NAT_1:13; then A52: x - (y + 1) >= 0 by XREAL_1:48; A53: ( rng (Del (g,(y + 1),x)) c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] ) ) proof rng (Del (g,(y + 1),x)) c= rng g by Th1; hence rng (Del (g,(y + 1),x)) c= rng F4() by A8, XBOOLE_1:1; ::_thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (Del (g,(y + 1),x)) implies P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] ) assume that A54: 1 <= i and A55: i < len (Del (g,(y + 1),x)) ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] percases ( i < y or i = y or i > y ) by XXREAL_0:1; supposeA56: i < y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] then i + 1 <= (y + 1) - 1 by NAT_1:13; then A57: (Del (g,(y + 1),x)) . (i + 1) = g . (i + 1) by A50, Th4, NAT_1:11; i <= (y + 1) - 1 by A56; then A58: (Del (g,(y + 1),x)) . i = g . i by A50, A54, Th4; i < len g by A49, A56, XXREAL_0:2; hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A54, A58, A57; ::_thesis: verum end; supposeA59: i = y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] now__::_thesis:_not_x_=_len_g assume x = len g ; ::_thesis: contradiction then y < (((len g) - (len g)) + (y + 1)) - 1 by A10, A50, A55, A59, Th2; hence contradiction ; ::_thesis: verum end; then A60: x < len g by A48, XXREAL_0:1; then A61: 0 < (len g) - x by XREAL_1:50; then 0 < (len g) -' x by XREAL_0:def_2; then 0 + 1 <= (len g) -' x by NAT_1:13; then 1 - 1 <= ((len g) -' x) - 1 by XREAL_1:9; then 0 <= ((len g) - x) - 1 by A61, XREAL_0:def_2; then (i + 1) + 0 <= (i + 1) + (((len g) - x) - 1) by XREAL_1:7; then (i + 1) + 0 <= ((i + 1) + ((len g) - x)) - 1 ; then A62: (Del (g,(y + 1),x)) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A10, A51, A50, A59, Th6 .= g . (x + 1) by A51, A59, XREAL_1:235 ; i <= (y + 1) - 1 by A59; then (Del (g,(y + 1),x)) . i = g . x by A12, A50, A54, A59, Th4; hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A46, A60, A62; ::_thesis: verum end; suppose i > y ; ::_thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] then A63: y + 1 <= i by NAT_1:13; A64: (len g) - x >= 0 by A48, XREAL_1:48; i < (((len g) - x) + (y + 1)) - 1 by A10, A50, A55, Th2; then A65: i < (((len g) -' x) + (y + 1)) - 1 by A64, XREAL_0:def_2; then i + 1 <= ((len g) -' x) + y by NAT_1:13; then i + 1 <= ((((len g) - x) + y) + 1) - 1 by A64, XREAL_0:def_2; then A66: i + 1 <= (((len g) - x) + (y + 1)) - 1 ; i < ((((len g) -' x) + y) + 1) - 1 by A65; then i < ((len g) - x) + y by A64, XREAL_0:def_2; then i - y < (((len g) - x) + y) - y by XREAL_1:9; then (i - y) + x < ((len g) - x) + x by XREAL_1:8; then (((x - y) - 1) + i) + 1 < len g ; then A67: ((x -' (y + 1)) + i) + 1 < len g by A52, XREAL_0:def_2; i <= i + 1 by NAT_1:11; then y + 1 <= i + 1 by A63, XXREAL_0:2; then A68: (Del (g,(y + 1),x)) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A10, A51, A50, A66, Th6 .= g . ((((x -' (y + 1)) + i) + 1) + 1) ; i <= (((len g) - x) + (y + 1)) - 1 by A10, A50, A55, Th2; then (Del (g,(y + 1),x)) . i = g . (((x -' (y + 1)) + i) + 1) by A10, A51, A50, A63, Th6; hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A68, A67, NAT_1:11; ::_thesis: verum end; end; end; A69: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) proof percases ( len (Del (g,(y + 1),x)) <= y or len (Del (g,(y + 1),x)) > y ) ; supposeA70: len (Del (g,(y + 1),x)) <= y ; ::_thesis: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) now__::_thesis:_not_len_(Del_(g,(y_+_1),x))_=_0 assume len (Del (g,(y + 1),x)) = 0 ; ::_thesis: contradiction then y + 1 = 0 + 1 by A10, A50, Th3; hence contradiction by A11, FINSEQ_3:24; ::_thesis: verum end; then A71: 0 + 1 <= len (Del (g,(y + 1),x)) by NAT_1:13; len (Del (g,(y + 1),x)) <= (y + 1) - 1 by A70; then A72: (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) = g . (len (Del (g,(y + 1),x))) by A50, A71, Th4; (((len g) - x) + (y + 1)) - 1 <= y by A10, A50, A70, Th2; then ((((len g) - x) + y) + 1) - 1 <= y ; then (len g) - x <= 0 by XREAL_1:29; then len g <= x by XREAL_1:50; then A73: len g = x by A48, XXREAL_0:1; then y <= (((len g) - x) + (y + 1)) - 1 ; hence F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) by A7, A10, A12, A50, A73, A72, Th2; ::_thesis: verum end; suppose len (Del (g,(y + 1),x)) > y ; ::_thesis: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) then A74: y + 1 <= len (Del (g,(y + 1),x)) by NAT_1:13; len (Del (g,(y + 1),x)) = (((len g) - x) + (y + 1)) - 1 by A10, A50, Th2; hence (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) = g . (((x -' (y + 1)) + ((((len g) - x) + (y + 1)) - 1)) + 1) by A10, A51, A50, A74, Th6 .= g . (((x - (y + 1)) + ((y + 1) + (((len g) - x) - 1))) + 1) by A51, XREAL_1:233 .= F2() by A7 ; ::_thesis: verum end; end; end; 1 <= (y + 1) - 1 by A11, FINSEQ_3:25; then A75: F1() = (Del (g,(y + 1),x)) . 1 by A6, A50, Th4; 0 < - (- (x - y)) by A45, XREAL_1:50; then - (x - y) < 0 ; then (len g) + (- (x - y)) < (len g) + 0 by XREAL_1:8; then (((len g) - x) + (y + 1)) - 1 < len g ; then len (Del (g,(y + 1),x)) < len g by A10, A50, Th2; hence contradiction by A4, A5, A75, A69, A53; ::_thesis: verum end; end; end; hence ex g being one-to-one FinSequence of F3() st ( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds P1[g . j,g . (j + 1)] ) ) by A6, A7, A8, A9; ::_thesis: verum end; begin theorem Th7: :: PENCIL_2:7 for I being non empty set for A being 1-sorted-yielding ManySortedSet of I for L being ManySortedSubset of Carrier A for i being Element of I for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A proof let I be non empty set ; ::_thesis: for A being 1-sorted-yielding ManySortedSet of I for L being ManySortedSubset of Carrier A for i being Element of I for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A let A be 1-sorted-yielding ManySortedSet of I; ::_thesis: for L being ManySortedSubset of Carrier A for i being Element of I for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A let L be ManySortedSubset of Carrier A; ::_thesis: for i being Element of I for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A let i be Element of I; ::_thesis: for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A let S be Subset of (A . i); ::_thesis: L +* (i,S) is ManySortedSubset of Carrier A A1: L c= Carrier A by PBOOLE:def_18; A2: dom L = I by PARTFUN1:def_2; L +* (i,S) c= Carrier A proof let a be set ; :: according to PBOOLE:def_2 ::_thesis: ( not a in I or (L +* (i,S)) . a c= (Carrier A) . a ) assume a in I ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a then reconsider b = a as Element of I ; percases ( a = i or a <> i ) ; supposeA3: a = i ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a then (L +* (i,S)) . b = S by A2, FUNCT_7:31; then (L +* (i,S)) . b c= the carrier of (A . b) by A3; hence (L +* (i,S)) . a c= (Carrier A) . a by YELLOW_6:2; ::_thesis: verum end; suppose a <> i ; ::_thesis: (L +* (i,S)) . a c= (Carrier A) . a then (L +* (i,S)) . a = L . b by FUNCT_7:32; hence (L +* (i,S)) . a c= (Carrier A) . a by A1, PBOOLE:def_2; ::_thesis: verum end; end; end; hence L +* (i,S) is ManySortedSubset of Carrier A by PBOOLE:def_18; ::_thesis: verum end; definition let I be non empty set ; let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; mode Segre-Coset of A -> Subset of (Segre_Product A) means :Def2: :: PENCIL_2:def 2 ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( it = product L & L . (indx L) = [#] (A . (indx L)) ); existence ex b1 being Subset of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( b1 = product L & L . (indx L) = [#] (A . (indx L)) ) proof set L = the non trivial-yielding Segre-like ManySortedSubset of Carrier A; reconsider C = the non trivial-yielding Segre-like ManySortedSubset of Carrier A +* ((indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A),([#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)))) as ManySortedSubset of Carrier A by Th7; A1: dom (Carrier A) = I by PARTFUN1:def_2; dom A = I by PARTFUN1:def_2; then A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) in rng A by FUNCT_1:3; then A2: not A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) is trivial by PENCIL_1:def_17; then reconsider C = C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:27; C c= Carrier A by PBOOLE:def_18; then A3: for a being set st a in I holds C . a c= (Carrier A) . a by PBOOLE:def_2; dom C = I by PARTFUN1:def_2; then reconsider P = product C as Subset of (Segre_Product A) by A1, A3, CARD_3:27; take P ; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( P = product L & L . (indx L) = [#] (A . (indx L)) ) dom the non trivial-yielding Segre-like ManySortedSubset of Carrier A = I by PARTFUN1:def_2; then A4: C . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) = [#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)) by FUNCT_7:31; then indx C = indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A by A2, PENCIL_1:def_21; hence ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( P = product L & L . (indx L) = [#] (A . (indx L)) ) by A4; ::_thesis: verum end; end; :: deftheorem Def2 defines Segre-Coset PENCIL_2:def_2_:_ for I being non empty set for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for b3 being Subset of (Segre_Product A) holds ( b3 is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( b3 = product L & L . (indx L) = [#] (A . (indx L)) ) ); theorem Th8: :: PENCIL_2:8 for I being non empty set for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds B1 = B2 proof let I be non empty set ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds B1 = B2 let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds B1 = B2 let B1, B2 be Segre-Coset of A; ::_thesis: ( 2 c= card (B1 /\ B2) implies B1 = B2 ) consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A1: B1 = product L1 and A2: L1 . (indx L1) = [#] (A . (indx L1)) by Def2; consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A3: B2 = product L2 and A4: L2 . (indx L2) = [#] (A . (indx L2)) by Def2; assume A5: 2 c= card (B1 /\ B2) ; ::_thesis: B1 = B2 then A6: indx L1 = indx L2 by A1, A3, PENCIL_1:26; A7: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ L1_._i_=_L2_._i let i be set ; ::_thesis: ( i in I implies L1 . b1 = L2 . b1 ) assume i in I ; ::_thesis: L1 . b1 = L2 . b1 percases ( i <> indx L1 or i = indx L1 ) ; suppose i <> indx L1 ; ::_thesis: L1 . b1 = L2 . b1 hence L1 . i = L2 . i by A5, A1, A3, PENCIL_1:26; ::_thesis: verum end; suppose i = indx L1 ; ::_thesis: L1 . b1 = L2 . b1 hence L1 . i = L2 . i by A2, A4, A6; ::_thesis: verum end; end; end; A8: dom L2 = I by PARTFUN1:def_2; dom L1 = I by PARTFUN1:def_2; hence B1 = B2 by A1, A3, A8, A7, FUNCT_1:2; ::_thesis: verum end; definition let S be TopStruct ; let X, Y be Subset of S; predX,Y are_joinable means :Def3: :: PENCIL_2:def 3 ex f being FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ); end; :: deftheorem Def3 defines are_joinable PENCIL_2:def_3_:_ for S being TopStruct for X, Y being Subset of S holds ( X,Y are_joinable iff ex f being FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) ); theorem :: PENCIL_2:9 for S being TopStruct for X, Y being Subset of S st X,Y are_joinable holds ex f being one-to-one FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) proof defpred S1[ set , set ] means 2 c= card ($1 /\ $2); let S be TopStruct ; ::_thesis: for X, Y being Subset of S st X,Y are_joinable holds ex f being one-to-one FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) let X, Y be Subset of S; ::_thesis: ( X,Y are_joinable implies ex f being one-to-one FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) ) assume X,Y are_joinable ; ::_thesis: ex f being one-to-one FinSequence of bool the carrier of S st ( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) then consider f being FinSequence of bool the carrier of S such that A1: ( X = f . 1 & Y = f . (len f) ) and A2: for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) and A3: for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) by Def3; A4: for i being Element of NAT for d1, d2 being set st 1 <= i & i < len f & d1 = f . i & d2 = f . (i + 1) holds S1[d1,d2] by A3; consider g being one-to-one FinSequence of bool the carrier of S such that A5: ( X = g . 1 & Y = g . (len g) ) and A6: rng g c= rng f and A7: for i being Element of NAT st 1 <= i & i < len g holds S1[g . i,g . (i + 1)] from PENCIL_2:sch_1(A1, A4); take g ; ::_thesis: ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds 2 c= card ((g . i) /\ (g . (i + 1))) ) ) thus ( X = g . 1 & Y = g . (len g) & ( for W being Subset of S st W in rng g holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len g holds 2 c= card ((g . i) /\ (g . (i + 1))) ) ) by A2, A5, A6, A7; ::_thesis: verum end; theorem Th10: :: PENCIL_2:10 for S being TopStruct for X being Subset of S st X is closed_under_lines & X is strong holds X,X are_joinable proof let S be TopStruct ; ::_thesis: for X being Subset of S st X is closed_under_lines & X is strong holds X,X are_joinable let X be Subset of S; ::_thesis: ( X is closed_under_lines & X is strong implies X,X are_joinable ) assume A1: ( X is closed_under_lines & X is strong ) ; ::_thesis: X,X are_joinable reconsider f = <*X*> as FinSequence of bool the carrier of S ; take f ; :: according to PENCIL_2:def_3 ::_thesis: ( X = f . 1 & X = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) thus X = f . 1 by FINSEQ_1:40; ::_thesis: ( X = f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) len f = 1 by FINSEQ_1:40; hence X = f . (len f) by FINSEQ_1:40; ::_thesis: ( ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) thus for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) proof let W be Subset of S; ::_thesis: ( W in rng f implies ( W is closed_under_lines & W is strong ) ) assume W in rng f ; ::_thesis: ( W is closed_under_lines & W is strong ) then W in {X} by FINSEQ_1:38; hence ( W is closed_under_lines & W is strong ) by A1, TARSKI:def_1; ::_thesis: verum end; let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies 2 c= card ((f . i) /\ (f . (i + 1))) ) assume that A2: 1 <= i and A3: i < len f ; ::_thesis: 2 c= card ((f . i) /\ (f . (i + 1))) thus 2 c= card ((f . i) /\ (f . (i + 1))) by A2, A3, FINSEQ_1:40; ::_thesis: verum end; theorem Th11: :: PENCIL_2:11 for I being non empty set for A being PLS-yielding ManySortedSet of I for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) let X, Y be Subset of (Segre_Product A); ::_thesis: ( not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable implies for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) ) assume that A1: ( not X is trivial & X is closed_under_lines & X is strong ) and A2: ( not Y is trivial & Y is closed_under_lines & Y is strong ) and A3: X,Y are_joinable ; ::_thesis: for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) set B = bool the carrier of (Segre_Product A); consider f being FinSequence of bool the carrier of (Segre_Product A) such that A4: X = f . 1 and A5: Y = f . (len f) and A6: for W being Subset of (Segre_Product A) st W in rng f holds ( W is closed_under_lines & W is strong ) and A7: for i being Element of NAT st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) by A3, Def3; len f in dom f by A2, A5, FUNCT_1:def_2; then A8: 1 <= len f by FINSEQ_3:25; consider B0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A9: X = product B0 and for C being Subset of (A . (indx B0)) st C = B0 . (indx B0) holds ( C is strong & C is closed_under_lines ) by A1, PENCIL_1:29; let X1, Y1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( X = product X1 & Y = product Y1 implies ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) ) assume that A10: X = product X1 and A11: Y = product Y1 ; ::_thesis: ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) defpred S1[ Element of NAT ] means for H being non trivial-yielding Segre-like ManySortedSubset of Carrier A st f . $1 = product H holds ( indx X1 = indx H & ( for i being set st i <> indx X1 holds X1 . i = H . i ) ); A12: B0 = X1 by A10, A9, PUA2MSS1:2; A13: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds S1[j + 1] proof let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] ) assume that A14: 1 <= j and A15: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] ) j in dom f by A14, A15, FINSEQ_3:25; then A16: f . j in rng f by FUNCT_1:3; A17: 1 <= j + 1 by NAT_1:11; j + 1 <= len f by A15, NAT_1:13; then j + 1 in dom f by A17, FINSEQ_3:25; then f . (j + 1) in rng f by FUNCT_1:3; then reconsider fj = f . j, fj1 = f . (j + 1) as Subset of (Segre_Product A) by A16; A18: card (fj /\ fj1) c= card fj by CARD_1:11, XBOOLE_1:17; A19: 2 c= card (fj /\ fj1) by A7, A14, A15; 2 c= card (fj /\ fj1) by A7, A14, A15; then 2 c= card fj by A18, XBOOLE_1:1; then ( not fj is trivial & fj is closed_under_lines & fj is strong ) by A6, A16, PENCIL_1:4; then consider B1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A20: fj = product B1 and for C being Subset of (A . (indx B1)) st C = B1 . (indx B1) holds ( C is strong & C is closed_under_lines ) by PENCIL_1:29; assume A21: S1[j] ; ::_thesis: S1[j + 1] then A22: indx B0 = indx B1 by A12, A20; now__::_thesis:_for_H_being_non_trivial-yielding_Segre-like_ManySortedSubset_of_Carrier_A_st_f_._(j_+_1)_=_product_H_holds_ (_indx_X1_=_indx_H_&_(_for_i_being_set_st_i_<>_indx_X1_holds_ X1_._i_=_H_._i_)_) let H be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( f . (j + 1) = product H implies ( indx X1 = indx H & ( for i being set st i <> indx X1 holds X1 . i = H . i ) ) ) assume A23: f . (j + 1) = product H ; ::_thesis: ( indx X1 = indx H & ( for i being set st i <> indx X1 holds X1 . i = H . i ) ) hence indx X1 = indx H by A12, A20, A22, A19, PENCIL_1:26; ::_thesis: for i being set st i <> indx X1 holds X1 . i = H . i thus for i being set st i <> indx X1 holds X1 . i = H . i ::_thesis: verum proof let i be set ; ::_thesis: ( i <> indx X1 implies X1 . i = H . i ) assume A24: i <> indx X1 ; ::_thesis: X1 . i = H . i then A25: i <> indx B1 by A21, A20; thus X1 . i = B1 . i by A21, A20, A24 .= H . i by A20, A19, A23, A25, PENCIL_1:26 ; ::_thesis: verum end; end; hence S1[j + 1] ; ::_thesis: verum end; A26: S1[1] by A10, A4, PUA2MSS1:2; for i being Element of NAT st 1 <= i & i <= len f holds S1[i] from INT_1:sch_7(A26, A13); hence ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds X1 . i = Y1 . i ) ) by A11, A5, A8; ::_thesis: verum end; begin theorem :: PENCIL_2:12 for S being 1-sorted for T being non empty 1-sorted for f being Function of S,T st f is bijective holds f " is bijective proof let S be 1-sorted ; ::_thesis: for T being non empty 1-sorted for f being Function of S,T st f is bijective holds f " is bijective let T be non empty 1-sorted ; ::_thesis: for f being Function of S,T st f is bijective holds f " is bijective let f be Function of S,T; ::_thesis: ( f is bijective implies f " is bijective ) assume A1: f is bijective ; ::_thesis: f " is bijective then A2: rng f = [#] T by FUNCT_2:def_3; then rng (f ") = [#] S by A1, TOPS_2:49; then A3: f " is onto by FUNCT_2:def_3; f " is one-to-one by A1, A2, TOPS_2:50; hence f " is bijective by A3; ::_thesis: verum end; definition let S, T be TopStruct ; let f be Function of S,T; attrf is isomorphic means :Def4: :: PENCIL_2:def 4 ( f is bijective & f is open & f " is bijective & f " is open ); end; :: deftheorem Def4 defines isomorphic PENCIL_2:def_4_:_ for S, T being TopStruct for f being Function of S,T holds ( f is isomorphic iff ( f is bijective & f is open & f " is bijective & f " is open ) ); registration let S be non empty TopStruct ; cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total isomorphic for Element of bool [: the carrier of S, the carrier of S:]; existence ex b1 being Function of S,S st b1 is isomorphic proof take f = id S; ::_thesis: f is isomorphic f " = id S by TOPGRP_1:2; hence f is isomorphic by Def4; ::_thesis: verum end; end; definition let S be non empty TopStruct ; mode Collineation of S is isomorphic Function of S,S; end; definition let S be non empty non void TopStruct ; let f be Collineation of S; let l be Block of S; :: original: .: redefine funcf .: l -> Block of S; coherence f .: l is Block of S proof l in the topology of S ; then reconsider L = l as Subset of S ; A1: L is open by PRE_TOPC:def_2; f is open by Def4; then f .: L is open by A1, T_0TOPSP:def_2; hence f .: l is Block of S by PRE_TOPC:def_2; ::_thesis: verum end; end; definition let S be non empty non void TopStruct ; let f be Collineation of S; let l be Block of S; :: original: " redefine funcf " l -> Block of S; coherence f " l is Block of S proof l in the topology of S ; then reconsider L = l as Subset of S ; A1: L is open by PRE_TOPC:def_2; A2: f is bijective by Def4; f " = f " by A2, TOPS_2:def_4; then A3: (f ") .: L = f " L by A2, FUNCT_1:85; f " is open by Def4; then (f ") .: L is open by A1, T_0TOPSP:def_2; hence f " l is Block of S by A3, PRE_TOPC:def_2; ::_thesis: verum end; end; theorem Th13: :: PENCIL_2:13 for S being non empty TopStruct for f being Collineation of S holds f " is Collineation of S proof let S be non empty TopStruct ; ::_thesis: for f being Collineation of S holds f " is Collineation of S let f be Collineation of S; ::_thesis: f " is Collineation of S A1: ( f " is bijective & f " is open ) by Def4; A2: f is bijective by Def4; then A3: rng f = [#] S by FUNCT_2:def_3; then (f ") " = f by A2, TOPS_2:51; then A4: (f ") " is open by Def4; (f ") " is bijective by A2, A3, TOPS_2:51; hence f " is Collineation of S by A1, A4, Def4; ::_thesis: verum end; theorem Th14: :: PENCIL_2:14 for S being non empty TopStruct for f being Collineation of S for X being Subset of S st not X is trivial holds not f .: X is trivial proof let S be non empty TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st not X is trivial holds not f .: X is trivial let f be Collineation of S; ::_thesis: for X being Subset of S st not X is trivial holds not f .: X is trivial let X be Subset of S; ::_thesis: ( not X is trivial implies not f .: X is trivial ) assume not X is trivial ; ::_thesis: not f .: X is trivial then 2 c= card X by PENCIL_1:4; then consider x, y being set such that A1: x in X and A2: y in X and A3: x <> y by PENCIL_1:2; A4: dom f = the carrier of S by FUNCT_2:def_1; then A5: f . x in f .: X by A1, FUNCT_1:def_6; A6: f . y in f .: X by A4, A2, FUNCT_1:def_6; f is bijective by Def4; then f . x <> f . y by A4, A1, A2, A3, FUNCT_1:def_4; then 2 c= card (f .: X) by A5, A6, PENCIL_1:2; hence not f .: X is trivial by PENCIL_1:4; ::_thesis: verum end; theorem :: PENCIL_2:15 for S being non empty TopStruct for f being Collineation of S for X being Subset of S st not X is trivial holds not f " X is trivial proof let S be non empty TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st not X is trivial holds not f " X is trivial let f be Collineation of S; ::_thesis: for X being Subset of S st not X is trivial holds not f " X is trivial let X be Subset of S; ::_thesis: ( not X is trivial implies not f " X is trivial ) assume not X is trivial ; ::_thesis: not f " X is trivial then 2 c= card X by PENCIL_1:4; then consider x, y being set such that A1: x in X and A2: y in X and A3: x <> y by PENCIL_1:2; f is bijective by Def4; then A4: rng f = the carrier of S by FUNCT_2:def_3; then consider fx being set such that A5: fx in dom f and A6: f . fx = x by A1, FUNCT_1:def_3; consider fy being set such that A7: fy in dom f and A8: f . fy = y by A4, A2, FUNCT_1:def_3; A9: fy in f " X by A2, A7, A8, FUNCT_1:def_7; fx in f " X by A1, A5, A6, FUNCT_1:def_7; then 2 c= card (f " X) by A3, A6, A8, A9, PENCIL_1:2; hence not f " X is trivial by PENCIL_1:4; ::_thesis: verum end; theorem Th16: :: PENCIL_2:16 for S being non empty non void TopStruct for f being Collineation of S for X being Subset of S st X is strong holds f .: X is strong proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st X is strong holds f .: X is strong let f be Collineation of S; ::_thesis: for X being Subset of S st X is strong holds f .: X is strong let X be Subset of S; ::_thesis: ( X is strong implies f .: X is strong ) assume A1: X is strong ; ::_thesis: f .: X is strong thus f .: X is strong ::_thesis: verum proof let a, b be Point of S; :: according to PENCIL_1:def_3 ::_thesis: ( not a in f .: X or not b in f .: X or a,b are_collinear ) assume that A2: a in f .: X and A3: b in f .: X ; ::_thesis: a,b are_collinear thus a,b are_collinear ::_thesis: verum proof percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: a,b are_collinear hence a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum end; supposeA4: a <> b ; ::_thesis: a,b are_collinear consider B being set such that A5: B in dom f and A6: B in X and A7: b = f . B by A3, FUNCT_1:def_6; consider A being set such that A8: A in dom f and A9: A in X and A10: a = f . A by A2, FUNCT_1:def_6; reconsider A = A, B = B as Point of S by A8, A5; A,B are_collinear by A1, A9, A6, PENCIL_1:def_3; then consider l being Block of S such that A11: {A,B} c= l by A4, A10, A7, PENCIL_1:def_1; B in l by A11, ZFMISC_1:32; then A12: b in f .: l by A5, A7, FUNCT_1:def_6; A in l by A11, ZFMISC_1:32; then a in f .: l by A8, A10, FUNCT_1:def_6; then {a,b} c= f .: l by A12, ZFMISC_1:32; hence a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum end; end; end; end; end; theorem :: PENCIL_2:17 for S being non empty non void TopStruct for f being Collineation of S for X being Subset of S st X is strong holds f " X is strong proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st X is strong holds f " X is strong let f be Collineation of S; ::_thesis: for X being Subset of S st X is strong holds f " X is strong reconsider g = f " as Collineation of S by Th13; let X be Subset of S; ::_thesis: ( X is strong implies f " X is strong ) assume X is strong ; ::_thesis: f " X is strong then A1: g .: X is strong by Th16; A2: f is bijective by Def4; then rng f = [#] S by FUNCT_2:def_3; hence f " X is strong by A2, A1, TOPS_2:55; ::_thesis: verum end; theorem Th18: :: PENCIL_2:18 for S being non empty non void TopStruct for f being Collineation of S for X being Subset of S st X is closed_under_lines holds f .: X is closed_under_lines proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st X is closed_under_lines holds f .: X is closed_under_lines let f be Collineation of S; ::_thesis: for X being Subset of S st X is closed_under_lines holds f .: X is closed_under_lines let X be Subset of S; ::_thesis: ( X is closed_under_lines implies f .: X is closed_under_lines ) assume A1: X is closed_under_lines ; ::_thesis: f .: X is closed_under_lines thus f .: X is closed_under_lines ::_thesis: verum proof let l be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( not 2 c= card (l /\ (f .: X)) or l c= f .: X ) assume 2 c= card (l /\ (f .: X)) ; ::_thesis: l c= f .: X then consider a, b being set such that A2: a in l /\ (f .: X) and A3: b in l /\ (f .: X) and A4: a <> b by PENCIL_1:2; b in f .: X by A3, XBOOLE_0:def_4; then consider B being set such that A5: B in dom f and A6: B in X and A7: b = f . B by FUNCT_1:def_6; b in l by A3, XBOOLE_0:def_4; then B in f " l by A5, A7, FUNCT_1:def_7; then A8: B in (f " l) /\ X by A6, XBOOLE_0:def_4; a in f .: X by A2, XBOOLE_0:def_4; then consider A being set such that A9: A in dom f and A10: A in X and A11: a = f . A by FUNCT_1:def_6; a in l by A2, XBOOLE_0:def_4; then A in f " l by A9, A11, FUNCT_1:def_7; then A in (f " l) /\ X by A10, XBOOLE_0:def_4; then 2 c= card ((f " l) /\ X) by A4, A11, A7, A8, PENCIL_1:2; then f " l c= X by A1, PENCIL_1:def_2; then A12: f .: (f " l) c= f .: X by RELAT_1:123; f is bijective by Def4; then A13: rng f = the carrier of S by FUNCT_2:def_3; l in the topology of S ; hence l c= f .: X by A13, A12, FUNCT_1:77; ::_thesis: verum end; end; theorem :: PENCIL_2:19 for S being non empty non void TopStruct for f being Collineation of S for X being Subset of S st X is closed_under_lines holds f " X is closed_under_lines proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X being Subset of S st X is closed_under_lines holds f " X is closed_under_lines let f be Collineation of S; ::_thesis: for X being Subset of S st X is closed_under_lines holds f " X is closed_under_lines reconsider g = f " as Collineation of S by Th13; let X be Subset of S; ::_thesis: ( X is closed_under_lines implies f " X is closed_under_lines ) assume X is closed_under_lines ; ::_thesis: f " X is closed_under_lines then A1: g .: X is closed_under_lines by Th18; A2: f is bijective by Def4; then rng f = [#] S by FUNCT_2:def_3; hence f " X is closed_under_lines by A2, A1, TOPS_2:55; ::_thesis: verum end; theorem Th20: :: PENCIL_2:20 for S being non empty non void TopStruct for f being Collineation of S for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f .: X,f .: Y are_joinable proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f .: X,f .: Y are_joinable let f be Collineation of S; ::_thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f .: X,f .: Y are_joinable let X, Y be Subset of S; ::_thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f .: X,f .: Y are_joinable ) assume that A1: not X is trivial and A2: not Y is trivial and A3: X,Y are_joinable ; ::_thesis: f .: X,f .: Y are_joinable consider g being FinSequence of bool the carrier of S such that A4: X = g . 1 and A5: Y = g . (len g) and A6: for W being Subset of S st W in rng g holds ( W is closed_under_lines & W is strong ) and A7: for i being Element of NAT st 1 <= i & i < len g holds 2 c= card ((g . i) /\ (g . (i + 1))) by A3, Def3; deffunc H1( set ) -> Element of bool the carrier of S = f .: (g . $1); consider p being FinSequence such that A8: ( len p = len g & ( for k being Nat st k in dom p holds p . k = H1(k) ) ) from FINSEQ_1:sch_2(); A9: dom g = Seg (len g) by FINSEQ_1:def_3; A10: dom p = Seg (len p) by FINSEQ_1:def_3; rng p c= bool the carrier of S proof let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in rng p or o in bool the carrier of S ) assume o in rng p ; ::_thesis: o in bool the carrier of S then consider i being set such that A11: i in dom p and A12: o = p . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A11; g . i in rng g by A8, A10, A9, A11, FUNCT_1:3; then reconsider gi = g . i as Subset of S ; p . i = f .: gi by A8, A11; hence o in bool the carrier of S by A12; ::_thesis: verum end; then reconsider p = p as FinSequence of bool the carrier of S by FINSEQ_1:def_4; take p ; :: according to PENCIL_2:def_3 ::_thesis: ( f .: X = p . 1 & f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds 2 c= card ((p . i) /\ (p . (i + 1))) ) ) 1 in dom g by A1, A4, FUNCT_1:def_2; hence f .: X = p . 1 by A4, A8, A10, A9; ::_thesis: ( f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds 2 c= card ((p . i) /\ (p . (i + 1))) ) ) len g in dom g by A2, A5, FUNCT_1:def_2; hence f .: Y = p . (len p) by A5, A8, A10, A9; ::_thesis: ( ( for W being Subset of S st W in rng p holds ( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds 2 c= card ((p . i) /\ (p . (i + 1))) ) ) thus for W being Subset of S st W in rng p holds ( W is closed_under_lines & W is strong ) ::_thesis: for i being Element of NAT st 1 <= i & i < len p holds 2 c= card ((p . i) /\ (p . (i + 1))) proof let W be Subset of S; ::_thesis: ( W in rng p implies ( W is closed_under_lines & W is strong ) ) assume W in rng p ; ::_thesis: ( W is closed_under_lines & W is strong ) then consider i being set such that A13: i in dom p and A14: W = p . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A13; g . i in rng g by A8, A10, A9, A13, FUNCT_1:3; then reconsider gi = g . i as Subset of S ; gi in rng g by A8, A10, A9, A13, FUNCT_1:3; then A15: ( gi is strong & gi is closed_under_lines ) by A6; p . i = f .: gi by A8, A13; hence ( W is closed_under_lines & W is strong ) by A14, A15, Th16, Th18; ::_thesis: verum end; A16: f is bijective by Def4; thus for i being Element of NAT st 1 <= i & i < len p holds 2 c= card ((p . i) /\ (p . (i + 1))) ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len p implies 2 c= card ((p . i) /\ (p . (i + 1))) ) assume that A17: 1 <= i and A18: i < len p ; ::_thesis: 2 c= card ((p . i) /\ (p . (i + 1))) A19: (g . i) /\ (g . (i + 1)) c= g . i by XBOOLE_1:17; i in dom g by A8, A17, A18, FINSEQ_3:25; then g . i in rng g by FUNCT_1:3; then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by A19, XBOOLE_1:1; 2 c= card ((g . i) /\ (g . (i + 1))) by A7, A8, A17, A18; then not gg is trivial by PENCIL_1:4; then not f .: gg is trivial by Th14; then A20: not (f .: (g . i)) /\ (f .: (g . (i + 1))) is trivial by A16, FUNCT_1:62; A21: i + 1 <= len p by A18, NAT_1:13; 1 <= i + 1 by A17, NAT_1:13; then i + 1 in dom p by A21, FINSEQ_3:25; then A22: p . (i + 1) = f .: (g . (i + 1)) by A8; i in dom g by A8, A17, A18, FINSEQ_3:25; then p . i = f .: (g . i) by A8, A10, A9; hence 2 c= card ((p . i) /\ (p . (i + 1))) by A22, A20, PENCIL_1:4; ::_thesis: verum end; end; theorem :: PENCIL_2:21 for S being non empty non void TopStruct for f being Collineation of S for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f " X,f " Y are_joinable proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f " X,f " Y are_joinable let f be Collineation of S; ::_thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds f " X,f " Y are_joinable let X, Y be Subset of S; ::_thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f " X,f " Y are_joinable ) reconsider g = f " as Collineation of S by Th13; assume that A1: not X is trivial and A2: not Y is trivial and A3: X,Y are_joinable ; ::_thesis: f " X,f " Y are_joinable A4: f is bijective by Def4; then A5: rng f = [#] S by FUNCT_2:def_3; then A6: f " Y = g .: Y by A4, TOPS_2:55; f " X = g .: X by A4, A5, TOPS_2:55; hence f " X,f " Y are_joinable by A6, A1, A2, A3, Th20; ::_thesis: verum end; theorem Th22: :: PENCIL_2:22 for I being non empty set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A let W be Subset of (Segre_Product A); ::_thesis: ( not W is trivial & W is strong & W is closed_under_lines implies union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A ) assume A2: ( not W is trivial & W is strong & W is closed_under_lines ) ; ::_thesis: union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A consider K being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A3: W = product K and A4: for S being Subset of (A . (indx K)) st S = K . (indx K) holds ( S is strong & S is closed_under_lines ) by A2, PENCIL_1:29; set O = [#] (A . (indx K)); set B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } c= the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } or a in the carrier of (Segre_Product A) ) assume a in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; ::_thesis: a in the carrier of (Segre_Product A) then consider y being set such that A5: a in y and A6: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by TARSKI:def_4; ex Y being Subset of (Segre_Product A) st ( y = Y & not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) by A6; hence a in the carrier of (Segre_Product A) by A5; ::_thesis: verum end; then reconsider C = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } as Subset of (Segre_Product A) ; dom A = I by PARTFUN1:def_2; then A . (indx K) in rng A by FUNCT_1:3; then A7: not A . (indx K) is trivial by PENCIL_1:def_17; then reconsider L = K +* ((indx K),([#] (A . (indx K)))) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th7, PENCIL_1:27; dom K = I by PARTFUN1:def_2; then L . (indx K) = [#] (A . (indx K)) by FUNCT_7:31; then A8: indx K = indx L by A7, PENCIL_1:def_21; A9: product L c= C proof K c= Carrier A by PBOOLE:def_18; then K . (indx K) c= (Carrier A) . (indx K) by PBOOLE:def_2; then reconsider S = K . (indx K) as Subset of (A . (indx K)) by YELLOW_6:2; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product L or y in C ) A10: dom K = I by PARTFUN1:def_2; A11: A . (indx K) is strongly_connected by A1; assume y in product L ; ::_thesis: y in C then consider z being Function such that A12: z = y and A13: dom z = dom L and A14: for a being set st a in dom L holds z . a in L . a by CARD_3:def_5; A15: dom L = I by PARTFUN1:def_2; then reconsider z = z as ManySortedSet of I by A13, PARTFUN1:def_2, RELAT_1:def_18; z . (indx K) in L . (indx K) by A14, A15; then reconsider zi = z . (indx K) as Point of (A . (indx K)) by A10, FUNCT_7:31; ( not S is trivial & S is strong & S is closed_under_lines ) by A4, PENCIL_1:def_21; then consider f being FinSequence of bool the carrier of (A . (indx K)) such that A16: S = f . 1 and A17: zi in f . (len f) and A18: for Z being Subset of (A . (indx K)) st Z in rng f holds ( Z is closed_under_lines & Z is strong ) and A19: for i being Nat st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) by A11, PENCIL_1:def_11; A20: len f in dom f by A17, FUNCT_1:def_2; then 1 in dom f by FINSEQ_5:6, RELAT_1:38; then A21: 1 in Seg (len f) by FINSEQ_1:def_3; A22: not f . (len f) is trivial proof reconsider l1 = (len f) - 1 as Element of NAT by A20, FINSEQ_3:26; A23: 1 <= len f by A20, FINSEQ_3:25; percases ( len f = 1 or len f > 1 ) by A23, XXREAL_0:1; suppose len f = 1 ; ::_thesis: not f . (len f) is trivial hence not f . (len f) is trivial by A16, PENCIL_1:def_21; ::_thesis: verum end; suppose len f > 1 ; ::_thesis: not f . (len f) is trivial then 1 + 1 <= len f by NAT_1:13; then A24: 2 - 1 <= l1 by XREAL_1:9; A25: card ((f . l1) /\ (f . (l1 + 1))) c= card (f . (l1 + 1)) by CARD_1:11, XBOOLE_1:17; l1 < (len f) - 0 by XREAL_1:15; then 2 c= card ((f . l1) /\ (f . (l1 + 1))) by A19, A24; then 2 c= card (f . (l1 + 1)) by A25, XBOOLE_1:1; hence not f . (len f) is trivial by PENCIL_1:4; ::_thesis: verum end; end; end; then reconsider ff = f . (len f) as non trivial set ; L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31; then indx K = indx L by A7, PENCIL_1:def_21; then reconsider EL = L +* ((indx K),ff) as non trivial-yielding Segre-like ManySortedSet of I by PENCIL_1:27; A26: dom z = dom (L +* ((indx K),(f . (len f)))) by A13, FUNCT_7:30; deffunc H1( set ) -> set = product (L +* ((indx K),(f . $1))); consider g being FinSequence such that A27: ( len g = len f & ( for k being Nat st k in dom g holds g . k = H1(k) ) ) from FINSEQ_1:sch_2(); A28: rng g c= bool the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in bool the carrier of (Segre_Product A) ) A29: dom (Carrier A) = I by PARTFUN1:def_2; assume a in rng g ; ::_thesis: a in bool the carrier of (Segre_Product A) then consider k being set such that A30: k in dom g and A31: a = g . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A30; A32: k in Seg (len f) by A27, A30, FINSEQ_1:def_3; A33: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ (L_+*_((indx_K),(f_._k)))_._o_c=_(Carrier_A)_._o let o be set ; ::_thesis: ( o in I implies (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1 ) assume A34: o in I ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1 A35: k in dom f by A32, FINSEQ_1:def_3; percases ( o <> indx K or o = indx K ) ; supposeA36: o <> indx K ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1 then (L +* ((indx K),(f . k))) . o = L . o by FUNCT_7:32; then A37: (L +* ((indx K),(f . k))) . o = K . o by A36, FUNCT_7:32; K c= Carrier A by PBOOLE:def_18; hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A34, A37, PBOOLE:def_2; ::_thesis: verum end; supposeA38: o = indx K ; ::_thesis: (L +* ((indx K),(f . k))) . b1 c= (Carrier A) . b1 then (L +* ((indx K),(f . k))) . o = f . k by A15, FUNCT_7:31; then (L +* ((indx K),(f . k))) . o in rng f by A35, FUNCT_1:3; then (L +* ((indx K),(f . k))) . o c= the carrier of (A . (indx K)) ; hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A38, YELLOW_6:2; ::_thesis: verum end; end; end; dom (L +* ((indx K),(f . k))) = I by PARTFUN1:def_2; then product (L +* ((indx K),(f . k))) c= product (Carrier A) by A29, A33, CARD_3:27; then a c= product (Carrier A) by A27, A30, A31; hence a in bool the carrier of (Segre_Product A) ; ::_thesis: verum end; A39: dom g = Seg (len f) by A27, FINSEQ_1:def_3; reconsider g = g as FinSequence of bool the carrier of (Segre_Product A) by A28, FINSEQ_1:def_4; len f in dom g by A20, A27, FINSEQ_3:29; then A40: g . (len f) in rng g by FUNCT_1:3; then reconsider Yb = g . (len f) as Subset of (Segre_Product A) ; A41: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ (L_+*_((indx_K),(f_._1)))_._o_=_K_._o let o be set ; ::_thesis: ( o in I implies (L +* ((indx K),(f . 1))) . b1 = K . b1 ) assume o in I ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1 percases ( o <> indx K or o = indx K ) ; supposeA42: o <> indx K ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1 then (L +* ((indx K),(f . 1))) . o = L . o by FUNCT_7:32; hence (L +* ((indx K),(f . 1))) . o = K . o by A42, FUNCT_7:32; ::_thesis: verum end; suppose o = indx K ; ::_thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1 hence (L +* ((indx K),(f . 1))) . o = K . o by A15, A16, FUNCT_7:31; ::_thesis: verum end; end; end; A43: for V being Subset of (Segre_Product A) st V in rng g holds ( V is closed_under_lines & V is strong ) proof let V be Subset of (Segre_Product A); ::_thesis: ( V in rng g implies ( V is closed_under_lines & V is strong ) ) assume V in rng g ; ::_thesis: ( V is closed_under_lines & V is strong ) then consider n1 being set such that A44: n1 in dom g and A45: V = g . n1 by FUNCT_1:def_3; reconsider n = n1 as Element of NAT by A44; n in Seg (len f) by A27, A44, FINSEQ_1:def_3; then A46: n in dom f by FINSEQ_1:def_3; not f . n is trivial proof A47: n <= len f by A46, FINSEQ_3:25; percases ( ( 1 <= n & n = len f ) or ( 1 <= n & n < len f ) ) by A46, A47, FINSEQ_3:25, XXREAL_0:1; suppose ( 1 <= n & n = len f ) ; ::_thesis: not f . n is trivial hence not f . n is trivial by A22; ::_thesis: verum end; supposeA48: ( 1 <= n & n < len f ) ; ::_thesis: not f . n is trivial A49: card ((f . n) /\ (f . (n + 1))) c= card (f . n) by CARD_1:11, XBOOLE_1:17; 2 c= card ((f . n) /\ (f . (n + 1))) by A19, A48; then 2 c= card (f . n) by A49, XBOOLE_1:1; hence not f . n is trivial by PENCIL_1:4; ::_thesis: verum end; end; end; then reconsider fn = f . n as non trivial set ; A50: L +* ((indx K),(f . n)) c= Carrier A proof let o be set ; :: according to PBOOLE:def_2 ::_thesis: ( not o in I or (L +* ((indx K),(f . n))) . o c= (Carrier A) . o ) assume A51: o in I ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o percases ( o <> indx K or o = indx K ) ; supposeA52: o <> indx K ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o A53: L c= Carrier A by PBOOLE:def_18; (L +* ((indx K),(f . n))) . o = L . o by A52, FUNCT_7:32; hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A51, A53, PBOOLE:def_2; ::_thesis: verum end; supposeA54: o = indx K ; ::_thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o then (L +* ((indx K),(f . n))) . o = f . n by A15, FUNCT_7:31; then (L +* ((indx K),(f . n))) . o in rng f by A46, FUNCT_1:3; then (L +* ((indx K),(f . n))) . o c= the carrier of (A . (indx K)) ; hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A54, YELLOW_6:2; ::_thesis: verum end; end; end; L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31; then indx K = indx L by A7, PENCIL_1:def_21; then reconsider LI = L +* ((indx K),fn) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A50, PBOOLE:def_18, PENCIL_1:27; reconsider LI = LI as non trivial-yielding Segre-like ManySortedSubset of Carrier A ; A55: LI . (indx K) = fn by A15, FUNCT_7:31; then A56: indx LI = indx K by PENCIL_1:def_21; A57: now__::_thesis:_for_D_being_Subset_of_(A_._(indx_LI))_st_D_=_LI_._(indx_LI)_holds_ (_D_is_strong_&_D_is_closed_under_lines_) let D be Subset of (A . (indx LI)); ::_thesis: ( D = LI . (indx LI) implies ( D is strong & D is closed_under_lines ) ) assume D = LI . (indx LI) ; ::_thesis: ( D is strong & D is closed_under_lines ) then D in rng f by A46, A55, A56, FUNCT_1:3; hence ( D is strong & D is closed_under_lines ) by A18, A56; ::_thesis: verum end; g . n = product (L +* ((indx K),(f . n))) by A27, A44; hence ( V is closed_under_lines & V is strong ) by A45, A57, PENCIL_1:29; ::_thesis: verum end; A58: len f in Seg (len f) by A20, FINSEQ_1:def_3; then Yb = product EL by A27, A39; then A59: ( not Yb is trivial & Yb is strong & Yb is closed_under_lines ) by A40, A43; A60: for i being Element of NAT st 1 <= i & i < len g holds 2 c= card ((g . i) /\ (g . (i + 1))) proof consider l1 being set such that A61: l1 in product L by XBOOLE_0:def_1; let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) ) assume that A62: 1 <= i and A63: i < len g ; ::_thesis: 2 c= card ((g . i) /\ (g . (i + 1))) i in Seg (len f) by A27, A62, A63, FINSEQ_1:1; then A64: g . i = product (L +* ((indx K),(f . i))) by A27, A39; 2 c= card ((f . i) /\ (f . (i + 1))) by A19, A27, A62, A63; then consider a, b being set such that A65: a in (f . i) /\ (f . (i + 1)) and A66: b in (f . i) /\ (f . (i + 1)) and A67: a <> b by PENCIL_1:2; consider l being Function such that l = l1 and A68: dom l = dom L and A69: for o being set st o in dom L holds l . o in L . o by A61, CARD_3:def_5; reconsider l = l as ManySortedSet of I by A15, A68, PARTFUN1:def_2, RELAT_1:def_18; set l1 = l +* ((indx K),a); set l2 = l +* ((indx K),b); A70: i + 1 <= len g by A63, NAT_1:13; A71: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._i)))_holds_ (l_+*_((indx_K),a))_._o_in_(L_+*_((indx_K),(f_._i)))_._o let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 ) assume o in dom (L +* ((indx K),(f . i))) ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 then A72: o in I ; then A73: o in dom l by PARTFUN1:def_2; percases ( o = indx K or o <> indx K ) ; supposeA74: o = indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 then (l +* ((indx K),a)) . o = a by A73, FUNCT_7:31; then (l +* ((indx K),a)) . o in f . i by A65, XBOOLE_0:def_4; hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A15, A74, FUNCT_7:31; ::_thesis: verum end; supposeA75: o <> indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 then A76: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32; l . o in L . o by A15, A69, A72; hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A75, A76, FUNCT_7:32; ::_thesis: verum end; end; end; 1 <= i + 1 by A62, NAT_1:13; then i + 1 in Seg (len f) by A27, A70, FINSEQ_1:1; then A77: g . (i + 1) = product (L +* ((indx K),(f . (i + 1)))) by A27, A39; A78: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._i)))_holds_ (l_+*_((indx_K),b))_._o_in_(L_+*_((indx_K),(f_._i)))_._o let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 ) assume o in dom (L +* ((indx K),(f . i))) ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 then A79: o in I ; then A80: o in dom l by PARTFUN1:def_2; percases ( o = indx K or o <> indx K ) ; supposeA81: o = indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 then (l +* ((indx K),b)) . o = b by A80, FUNCT_7:31; then (l +* ((indx K),b)) . o in f . i by A66, XBOOLE_0:def_4; hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A15, A81, FUNCT_7:31; ::_thesis: verum end; supposeA82: o <> indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 then A83: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32; l . o in L . o by A15, A69, A79; hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A82, A83, FUNCT_7:32; ::_thesis: verum end; end; end; A84: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(i_+_1))))_holds_ (l_+*_((indx_K),a))_._o_in_(L_+*_((indx_K),(f_._(i_+_1))))_._o let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 ) assume o in dom (L +* ((indx K),(f . (i + 1)))) ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then A85: o in I ; then A86: o in dom l by PARTFUN1:def_2; percases ( o = indx K or o <> indx K ) ; supposeA87: o = indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then (l +* ((indx K),a)) . o = a by A86, FUNCT_7:31; then (l +* ((indx K),a)) . o in f . (i + 1) by A65, XBOOLE_0:def_4; hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A87, FUNCT_7:31; ::_thesis: verum end; supposeA88: o <> indx K ; ::_thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then A89: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32; l . o in L . o by A15, A69, A85; hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A88, A89, FUNCT_7:32; ::_thesis: verum end; end; end; dom (l +* ((indx K),a)) = I by PARTFUN1:def_2 .= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def_2 ; then A90: l +* ((indx K),a) in product (L +* ((indx K),(f . (i + 1)))) by A84, CARD_3:9; A91: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(i_+_1))))_holds_ (l_+*_((indx_K),b))_._o_in_(L_+*_((indx_K),(f_._(i_+_1))))_._o let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 ) assume o in dom (L +* ((indx K),(f . (i + 1)))) ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then A92: o in I ; then A93: o in dom l by PARTFUN1:def_2; percases ( o = indx K or o <> indx K ) ; supposeA94: o = indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then (l +* ((indx K),b)) . o = b by A93, FUNCT_7:31; then (l +* ((indx K),b)) . o in f . (i + 1) by A66, XBOOLE_0:def_4; hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A94, FUNCT_7:31; ::_thesis: verum end; supposeA95: o <> indx K ; ::_thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 then A96: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32; l . o in L . o by A15, A69, A92; hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A95, A96, FUNCT_7:32; ::_thesis: verum end; end; end; dom (l +* ((indx K),b)) = I by PARTFUN1:def_2 .= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def_2 ; then A97: l +* ((indx K),b) in product (L +* ((indx K),(f . (i + 1)))) by A91, CARD_3:9; dom (l +* ((indx K),b)) = I by PARTFUN1:def_2 .= dom (L +* ((indx K),(f . i))) by PARTFUN1:def_2 ; then l +* ((indx K),b) in product (L +* ((indx K),(f . i))) by A78, CARD_3:9; then A98: l +* ((indx K),b) in (g . i) /\ (g . (i + 1)) by A64, A77, A97, XBOOLE_0:def_4; (l +* ((indx K),a)) . (indx K) = a by A15, A68, FUNCT_7:31; then A99: l +* ((indx K),a) <> l +* ((indx K),b) by A15, A67, A68, FUNCT_7:31; dom (l +* ((indx K),a)) = I by PARTFUN1:def_2 .= dom (L +* ((indx K),(f . i))) by PARTFUN1:def_2 ; then l +* ((indx K),a) in product (L +* ((indx K),(f . i))) by A71, CARD_3:9; then l +* ((indx K),a) in (g . i) /\ (g . (i + 1)) by A64, A77, A90, XBOOLE_0:def_4; hence 2 c= card ((g . i) /\ (g . (i + 1))) by A99, A98, PENCIL_1:2; ::_thesis: verum end; A100: now__::_thesis:_for_o_being_set_st_o_in_dom_(L_+*_((indx_K),(f_._(len_f))))_holds_ z_._o_in_(L_+*_((indx_K),(f_._(len_f))))_._o let o be set ; ::_thesis: ( o in dom (L +* ((indx K),(f . (len f)))) implies z . b1 in (L +* ((indx K),(f . (len f)))) . b1 ) assume o in dom (L +* ((indx K),(f . (len f)))) ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1 then A101: o in I ; percases ( o = indx K or o <> indx K ) ; suppose o = indx K ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1 hence z . o in (L +* ((indx K),(f . (len f)))) . o by A15, A17, FUNCT_7:31; ::_thesis: verum end; supposeA102: o <> indx K ; ::_thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1 z . o in L . o by A14, A15, A101; hence z . o in (L +* ((indx K),(f . (len f)))) . o by A102, FUNCT_7:32; ::_thesis: verum end; end; end; dom (L +* ((indx K),(f . 1))) = I by PARTFUN1:def_2; then L +* ((indx K),(f . 1)) = K by A10, A41, FUNCT_1:2; then W = g . 1 by A3, A27, A39, A21; then W,Yb are_joinable by A27, A43, A60, Def3; then A103: Yb in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A59; Yb = product (L +* ((indx K),(f . (len f)))) by A27, A39, A58; then y in Yb by A12, A26, A100, CARD_3:9; hence y in C by A103, TARSKI:def_4; ::_thesis: verum end; dom K = I by PARTFUN1:def_2; then A104: L . (indx L) = [#] (A . (indx L)) by A8, FUNCT_7:31; C c= product L proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in product L ) assume c in C ; ::_thesis: c in product L then consider y being set such that A105: c in y and A106: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by TARSKI:def_4; consider Y being Subset of (Segre_Product A) such that A107: y = Y and A108: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and A109: W,Y are_joinable by A106; reconsider c1 = c as ManySortedSet of I by A105, A107, PENCIL_1:14; consider M being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A110: Y = product M and for S being Subset of (A . (indx M)) st S = M . (indx M) holds ( S is strong & S is closed_under_lines ) by A108, PENCIL_1:29; A111: dom M = I by PARTFUN1:def_2 .= dom L by PARTFUN1:def_2 ; A112: dom K = I by PARTFUN1:def_2 .= dom L by PARTFUN1:def_2 ; A113: for a being set st a in dom L holds c1 . a in L . a proof let a be set ; ::_thesis: ( a in dom L implies c1 . a in L . a ) assume A114: a in dom L ; ::_thesis: c1 . a in L . a then reconsider a1 = a as Element of I ; percases ( a = indx K or a <> indx K ) ; supposeA115: a = indx K ; ::_thesis: c1 . a in L . a M c= Carrier A by PBOOLE:def_18; then M . a1 c= (Carrier A) . a1 by PBOOLE:def_2; then A116: M . a1 c= the carrier of (A . a1) by YELLOW_6:2; c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9; then c1 . a in [#] (A . (indx K)) by A115, A116; hence c1 . a in L . a by A112, A114, A115, FUNCT_7:31; ::_thesis: verum end; supposeA117: a <> indx K ; ::_thesis: c1 . a in L . a c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9; then c1 . a in K . a by A2, A3, A108, A109, A110, A117, Th11; hence c1 . a in L . a by A117, FUNCT_7:32; ::_thesis: verum end; end; end; dom c1 = I by PARTFUN1:def_2 .= dom L by PARTFUN1:def_2 ; hence c in product L by A113, CARD_3:9; ::_thesis: verum end; then C = product L by A9, XBOOLE_0:def_10; hence union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A by A104, Def2; ::_thesis: verum end; theorem Th23: :: PENCIL_2:23 for I being non empty set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being set holds ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being set holds ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being set holds ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being set holds ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) let B be set ; ::_thesis: ( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) thus ( B is Segre-Coset of A implies ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) ::_thesis: ( ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) implies B is Segre-Coset of A ) proof assume B is Segre-Coset of A ; ::_thesis: ex W being Subset of (Segre_Product A) st ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) then reconsider BB = B as Segre-Coset of A ; consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A2: BB = product L and A3: L . (indx L) = [#] (A . (indx L)) by Def2; set K1 = the Block of (A . (indx L)); consider V being set such that A4: V in product L by XBOOLE_0:def_1; the Block of (A . (indx L)) in the topology of (A . (indx L)) ; then reconsider K = the Block of (A . (indx L)) as Subset of (A . (indx L)) ; A5: ex g being Function st ( g = V & dom g = dom L & ( for i being set st i in dom L holds g . i in L . i ) ) by A4, CARD_3:def_5; A6: dom L = I by PARTFUN1:def_2; then reconsider V = V as ManySortedSet of I by A5, PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in I holds V . i is Element of (Carrier A) . i proof let i be set ; ::_thesis: ( i in I implies V . i is Element of (Carrier A) . i ) assume A7: i in I ; ::_thesis: V . i is Element of (Carrier A) . i L c= Carrier A by PBOOLE:def_18; then A8: L . i c= (Carrier A) . i by A7, PBOOLE:def_2; V . i in L . i by A6, A5, A7; hence V . i is Element of (Carrier A) . i by A8; ::_thesis: verum end; then reconsider V = V as Element of Carrier A by PBOOLE:def_14; reconsider VV = {V} as ManySortedSubset of Carrier A by PENCIL_1:11; reconsider X = VV +* ((indx L),K) as ManySortedSubset of Carrier A by Th7; 2 c= card K by PENCIL_1:def_6; then A9: not K is trivial by PENCIL_1:4; then reconsider X = X as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10; dom VV = I by PARTFUN1:def_2; then A10: X . (indx L) = K by FUNCT_7:31; then indx X = indx L by A9, PENCIL_1:def_21; then reconsider pX = product X as Block of (Segre_Product A) by A10, PENCIL_1:24; A11: for i being set st i in I holds X . i c= L . i proof let i be set ; ::_thesis: ( i in I implies X . i c= L . i ) assume A12: i in I ; ::_thesis: X . i c= L . i percases ( i <> indx L or i = indx L ) ; suppose i <> indx L ; ::_thesis: X . i c= L . i then X . i = VV . i by FUNCT_7:32; then A13: X . i = {(V . i)} by A12, PZFMISC1:def_1; V . i in L . i by A6, A5, A12; hence X . i c= L . i by A13, ZFMISC_1:31; ::_thesis: verum end; suppose i = indx L ; ::_thesis: X . i c= L . i hence X . i c= L . i by A3, A10; ::_thesis: verum end; end; end; pX in the topology of (Segre_Product A) ; then reconsider psX = pX as Subset of (Segre_Product A) ; take psX ; ::_thesis: ( not psX is trivial & psX is strong & psX is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } ) thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by PENCIL_1:20, PENCIL_1:21; ::_thesis: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } then reconsider Z = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } as Segre-Coset of A by A1, Th22; psX,psX are_joinable by A14, Th10; then A15: psX in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } by A14; A16: psX c= Z proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in psX or a in Z ) assume a in psX ; ::_thesis: a in Z hence a in Z by A15, TARSKI:def_4; ::_thesis: verum end; dom X = I by PARTFUN1:def_2; then psX c= B by A2, A6, A11, CARD_3:27; then psX c= B /\ Z by A16, XBOOLE_1:19; then A17: card psX c= card (B /\ Z) by CARD_1:11; 2 c= card pX by PENCIL_1:def_6; then BB = Z by A17, Th8, XBOOLE_1:1; hence B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } ; ::_thesis: verum end; given W being Subset of (Segre_Product A) such that A18: ( not W is trivial & W is strong & W is closed_under_lines ) and A19: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; ::_thesis: B is Segre-Coset of A thus B is Segre-Coset of A by A1, A18, A19, Th22; ::_thesis: verum end; theorem Th24: :: PENCIL_2:24 for I being non empty set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A let B be Segre-Coset of A; ::_thesis: for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A consider W being Subset of (Segre_Product A) such that A2: ( not W is trivial & W is strong & W is closed_under_lines ) and A3: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A1, Th23; let f be Collineation of (Segre_Product A); ::_thesis: f .: B is Segre-Coset of A reconsider g = f " as Collineation of (Segre_Product A) by Th13; A4: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; A5: dom g = the carrier of (Segre_Product A) by FUNCT_2:def_1; A6: f is bijective by Def4; then A7: rng f = the carrier of (Segre_Product A) by FUNCT_2:def_3; A8: rng f = [#] (Segre_Product A) by A6, FUNCT_2:def_3; A9: f .: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } proof A10: W c= f " (f .: W) by A4, FUNCT_1:76; f " (f .: W) c= W by A6, FUNCT_1:82; then A11: f " (f .: W) = W by A10, XBOOLE_0:def_10; thus f .: B c= union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } :: according to XBOOLE_0:def_10 ::_thesis: union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } c= f .: B proof let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in f .: B or o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } ) assume o in f .: B ; ::_thesis: o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } then consider u being set such that A12: u in dom f and A13: u in B and A14: o = f . u by FUNCT_1:def_6; consider y being set such that A15: u in y and A16: y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by A3, A13, TARSKI:def_4; consider Y being Subset of (Segre_Product A) such that A17: y = Y and A18: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and A19: W,Y are_joinable by A16; A20: f .: W,f .: Y are_joinable by A2, A18, A19, Th20; ( not f .: Y is trivial & f .: Y is strong & f .: Y is closed_under_lines ) by A18, Th14, Th16, Th18; then A21: f .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & f .: W,Z are_joinable ) } by A20; o in f .: Y by A12, A14, A15, A17, FUNCT_1:def_6; hence o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by A21, TARSKI:def_4; ::_thesis: verum end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } or o in f .: B ) assume o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } ; ::_thesis: o in f .: B then consider u being set such that A22: o in u and A23: u in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by TARSKI:def_4; consider Y being Subset of (Segre_Product A) such that A24: u = Y and A25: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and A26: f .: W,Y are_joinable by A23; A27: ( not g .: Y is trivial & g .: Y is strong & g .: Y is closed_under_lines ) by A25, Th14, Th16, Th18; ( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18; then g .: (f .: W),g .: Y are_joinable by A25, A26, Th20; then W,g .: Y are_joinable by A6, A8, A11, TOPS_2:55; then A28: g .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & W,Z are_joinable ) } by A27; g . o in g .: Y by A5, A22, A24, FUNCT_1:def_6; then A29: g . o in B by A3, A28, TARSKI:def_4; o = f . ((f ") . o) by A6, A7, A22, A24, FUNCT_1:35; then o = f . (g . o) by A6, TOPS_2:def_4; hence o in f .: B by A4, A29, FUNCT_1:def_6; ::_thesis: verum end; ( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18; hence f .: B is Segre-Coset of A by A1, A9, Th23; ::_thesis: verum end; theorem :: PENCIL_2:25 for I being non empty set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for B being Segre-Coset of A for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A let B be Segre-Coset of A; ::_thesis: for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A let f be Collineation of (Segre_Product A); ::_thesis: f " B is Segre-Coset of A reconsider g = f " as Collineation of (Segre_Product A) by Th13; A2: f is bijective by Def4; then rng f = [#] (Segre_Product A) by FUNCT_2:def_3; then f " B = g .: B by A2, TOPS_2:55; hence f " B is Segre-Coset of A by A1, Th24; ::_thesis: verum end;