:: PENCIL_2 semantic presentation

definition
let c1 be set ;
let c2 be FinSequence of c1;
let c3, c4 be Nat;
func Del c2,c3,c4 -> FinSequence of a1 equals :: PENCIL_2:def 1
(a2 | (a3 -' 1)) ^ (a2 /^ a4);
coherence
(c2 | (c3 -' 1)) ^ (c2 /^ c4) is FinSequence of c1 ;
end;

:: deftheorem Def1 defines Del PENCIL_2:def 1 :
for b1 being set
for b2 being FinSequence of b1
for b3, b4 being Nat holds Del b2,b3,b4 = (b2 | (b3 -' 1)) ^ (b2 /^ b4);

theorem Th1: :: PENCIL_2:1
for b1 being set
for b2 being FinSequence of b1
for b3, b4 being Nat holds rng (Del b2,b3,b4) c= rng b2
proof end;

theorem Th2: :: PENCIL_2:2
for b1 being set
for b2 being FinSequence of b1
for b3, b4 being Nat st b3 in dom b2 & b4 in dom b2 holds
len (Del b2,b3,b4) = (((len b2) - b4) + b3) - 1
proof end;

theorem Th3: :: PENCIL_2:3
for b1 being set
for b2 being FinSequence of b1
for b3, b4 being Nat st b3 in dom b2 & b4 in dom b2 & len (Del b2,b3,b4) = 0 holds
( b3 = 1 & b4 = len b2 )
proof end;

theorem Th4: :: PENCIL_2:4
for b1 being set
for b2 being FinSequence of b1
for b3, b4, b5 being Nat st b3 in dom b2 & 1 <= b5 & b5 <= b3 - 1 holds
(Del b2,b3,b4) . b5 = b2 . b5
proof end;

theorem Th5: :: PENCIL_2:5
for b1, b2 being FinSequence
for b3 being Nat st (len b1) + 1 <= b3 holds
(b1 ^ b2) . b3 = b2 . (b3 - (len b1))
proof end;

theorem Th6: :: PENCIL_2:6
for b1 being set
for b2 being FinSequence of b1
for b3, b4, b5 being Nat st b3 in dom b2 & b4 in dom b2 & b3 <= b4 & b3 <= b5 & b5 <= (((len b2) - b4) + b3) - 1 holds
(Del b2,b3,b4) . b5 = b2 . (((b4 -' b3) + b5) + 1)
proof end;

scheme :: PENCIL_2:sch 1
s1{ F1() -> set , F2() -> set , F3() -> set , F4() -> FinSequence of F3(), P1[ set , set ] } :
ex b1 being one-to-one FinSequence of F3() st
( F1() = b1 . 1 & F2() = b1 . (len b1) & rng b1 c= rng F4() & ( for b2 being Nat st 1 <= b2 & b2 < len b1 holds
P1[b1 . b2,b1 . (b2 + 1)] ) )
provided
E7: ( F1() = F4() . 1 & F2() = F4() . (len F4()) ) and
E8: for b1 being Nat
for b2, b3 being set st 1 <= b1 & b1 < len F4() & b2 = F4() . b1 & b3 = F4() . (b1 + 1) holds
P1[b2,b3]
proof end;

theorem Th7: :: PENCIL_2:7
for b1 being non empty set
for b2 being 1-sorted-yielding ManySortedSet of b1
for b3 being ManySortedSubset of Carrier b2
for b4 being Element of b1
for b5 being Subset of (b2 . b4) holds b3 +* b4,b5 is ManySortedSubset of Carrier b2
proof end;

definition
let c1 be non empty set ;
let c2 be TopStruct-yielding non-Trivial-yielding ManySortedSet of c1;
mode Segre-Coset of c2 -> Subset of (Segre_Product a2) means :Def2: :: PENCIL_2:def 2
ex b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier a2 st
( a3 = product b1 & b1 . (indx b1) = [#] (a2 . (indx b1)) );
existence
ex b1 being Subset of (Segre_Product c2)ex b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier c2 st
( b1 = product b2 & b2 . (indx b2) = [#] (c2 . (indx b2)) )
proof end;
end;

:: deftheorem Def2 defines Segre-Coset PENCIL_2:def 2 :
for b1 being non empty set
for b2 being TopStruct-yielding non-Trivial-yielding ManySortedSet of b1
for b3 being Subset of (Segre_Product b2) holds
( b3 is Segre-Coset of b2 iff ex b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier b2 st
( b3 = product b4 & b4 . (indx b4) = [#] (b2 . (indx b4)) ) );

theorem Th8: :: PENCIL_2:8
for b1 being non empty set
for b2 being TopStruct-yielding non-Trivial-yielding ManySortedSet of b1
for b3, b4 being Segre-Coset of b2 st 2 c= Card (b3 /\ b4) holds
b3 = b4
proof end;

definition
let c1 be TopStruct ;
let c2, c3 be Subset of c1;
pred c2,c3 are_joinable means :Def3: :: PENCIL_2:def 3
ex b1 being FinSequence of bool the carrier of a1 st
( a2 = b1 . 1 & a3 = b1 . (len b1) & ( for b2 being Subset of a1 st b2 in rng b1 holds
( b2 is closed_under_lines & b2 is strong ) ) & ( for b2 being Nat st 1 <= b2 & b2 < len b1 holds
2 c= Card ((b1 . b2) /\ (b1 . (b2 + 1))) ) );
end;

:: deftheorem Def3 defines are_joinable PENCIL_2:def 3 :
for b1 being TopStruct
for b2, b3 being Subset of b1 holds
( b2,b3 are_joinable iff ex b4 being FinSequence of bool the carrier of b1 st
( b2 = b4 . 1 & b3 = b4 . (len b4) & ( for b5 being Subset of b1 st b5 in rng b4 holds
( b5 is closed_under_lines & b5 is strong ) ) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 holds
2 c= Card ((b4 . b5) /\ (b4 . (b5 + 1))) ) ) );

theorem Th9: :: PENCIL_2:9
for b1 being TopStruct
for b2, b3 being Subset of b1 st b2,b3 are_joinable holds
ex b4 being one-to-one FinSequence of bool the carrier of b1 st
( b2 = b4 . 1 & b3 = b4 . (len b4) & ( for b5 being Subset of b1 st b5 in rng b4 holds
( b5 is closed_under_lines & b5 is strong ) ) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 holds
2 c= Card ((b4 . b5) /\ (b4 . (b5 + 1))) ) )
proof end;

theorem Th10: :: PENCIL_2:10
for b1 being TopStruct
for b2 being Subset of b1 st b2 is closed_under_lines & b2 is strong holds
b2,b2 are_joinable
proof end;

theorem Th11: :: PENCIL_2:11
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1
for b3, b4 being Subset of (Segre_Product b2) st not b3 is trivial & b3 is closed_under_lines & b3 is strong & not b4 is trivial & b4 is closed_under_lines & b4 is strong & b3,b4 are_joinable holds
for b5, b6 being non trivial-yielding Segre-like ManySortedSubset of Carrier b2 st b3 = product b5 & b4 = product b6 holds
( indx b5 = indx b6 & ( for b7 being set st b7 <> indx b5 holds
b5 . b7 = b6 . b7 ) )
proof end;

theorem Th12: :: PENCIL_2:12
for b1 being 1-sorted
for b2 being non empty 1-sorted
for b3 being Function of b1,b2 st b3 is bijective holds
b3 " is bijective
proof end;

definition
let c1, c2 be TopStruct ;
let c3 be Function of c1,c2;
attr a3 is isomorphic means :Def4: :: PENCIL_2:def 4
( a3 is bijective & a3 is open & a3 " is bijective & a3 " is open );
end;

:: deftheorem Def4 defines isomorphic PENCIL_2:def 4 :
for b1, b2 being TopStruct
for b3 being Function of b1,b2 holds
( b3 is isomorphic iff ( b3 is bijective & b3 is open & b3 " is bijective & b3 " is open ) );

registration
let c1 be non empty TopStruct ;
cluster isomorphic M5(the carrier of a1,the carrier of a1);
existence
ex b1 being Function of c1,c1 st b1 is isomorphic
proof end;
end;

definition
let c1 be non empty TopStruct ;
mode Collineation of a1 is isomorphic Function of a1,a1;
end;

definition
let c1 be non empty non void TopStruct ;
let c2 be Collineation of c1;
let c3 be Block of c1;
redefine func .: as c2 .: c3 -> Block of a1;
coherence
c2 .: c3 is Block of c1
proof end;
end;

definition
let c1 be non empty non void TopStruct ;
let c2 be Collineation of c1;
let c3 be Block of c1;
redefine func " as c2 " c3 -> Block of a1;
coherence
c2 " c3 is Block of c1
proof end;
end;

theorem Th13: :: PENCIL_2:13
for b1 being non empty TopStruct
for b2 being Collineation of b1 holds b2 " is Collineation of b1
proof end;

theorem Th14: :: PENCIL_2:14
for b1 being non empty TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st not b3 is trivial holds
not b2 .: b3 is trivial
proof end;

theorem Th15: :: PENCIL_2:15
for b1 being non empty TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st not b3 is trivial holds
not b2 " b3 is trivial
proof end;

theorem Th16: :: PENCIL_2:16
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st b3 is strong holds
b2 .: b3 is strong
proof end;

theorem Th17: :: PENCIL_2:17
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st b3 is strong holds
b2 " b3 is strong
proof end;

theorem Th18: :: PENCIL_2:18
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st b3 is closed_under_lines holds
b2 .: b3 is closed_under_lines
proof end;

theorem Th19: :: PENCIL_2:19
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3 being Subset of b1 st b3 is closed_under_lines holds
b2 " b3 is closed_under_lines
proof end;

theorem Th20: :: PENCIL_2:20
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3, b4 being Subset of b1 st not b3 is trivial & not b4 is trivial & b3,b4 are_joinable holds
b2 .: b3,b2 .: b4 are_joinable
proof end;

theorem Th21: :: PENCIL_2:21
for b1 being non empty non void TopStruct
for b2 being Collineation of b1
for b3, b4 being Subset of b1 st not b3 is trivial & not b4 is trivial & b3,b4 are_joinable holds
b2 " b3,b2 " b4 are_joinable
proof end;

theorem Th22: :: PENCIL_2:22
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds b2 . b3 is strongly_connected ) holds
for b3 being Subset of (Segre_Product b2) st not b3 is trivial & b3 is strong & b3 is closed_under_lines holds
union { b4 where B is Subset of (Segre_Product b2) : ( not b4 is trivial & b4 is strong & b4 is closed_under_lines & b3,b4 are_joinable ) } is Segre-Coset of b2
proof end;

theorem Th23: :: PENCIL_2:23
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds b2 . b3 is strongly_connected ) holds
for b3 being set holds
( b3 is Segre-Coset of b2 iff ex b4 being Subset of (Segre_Product b2) st
( not b4 is trivial & b4 is strong & b4 is closed_under_lines & b3 = union { b5 where B is Subset of (Segre_Product b2) : ( not b5 is trivial & b5 is strong & b5 is closed_under_lines & b4,b5 are_joinable ) } ) )
proof end;

theorem Th24: :: PENCIL_2:24
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds b2 . b3 is strongly_connected ) holds
for b3 being Segre-Coset of b2
for b4 being Collineation of (Segre_Product b2) holds b4 .: b3 is Segre-Coset of b2
proof end;

theorem Th25: :: PENCIL_2:25
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds b2 . b3 is strongly_connected ) holds
for b3 being Segre-Coset of b2
for b4 being Collineation of (Segre_Product b2) holds b4 " b3 is Segre-Coset of b2
proof end;