PENCIL

:: PENCIL_4 semantic presentation

begin

for k, n being ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) st k : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) < n : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) & 3 : ( ( ) ( non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) & not k : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) + 1 : ( ( ) ( non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < n : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) holds
2 : ( ( ) ( non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= k : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Nat) ;

theorem :: PENCIL_4:2

theorem :: PENCIL_4:3

theorem :: PENCIL_4:4

theorem :: PENCIL_4:5

definition

func segment (W1,W2) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: PENCIL_4:def 1
for W being ( ( strict ) ( non empty V65() strict V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) holds
( W : ( ( strict ) ( non empty V65() strict V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) in it : ( ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ( W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of W : ( ( strict ) ( non empty V65() strict V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) ) & W : ( ( strict ) ( non empty V65() strict V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) is ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ) ) if W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) )
otherwise it : ( ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( ) set ) ;

end;

theorem :: PENCIL_4:6

definition

func pencil (W1,W2) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: PENCIL_4:def 2
(segment (W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \ {((Omega). W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty V65() strict V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,((Omega). W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) : ( ( strict ) ( non empty V65() strict V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() ) Subspace of W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) } : ( ( ) ( finite ) set ) : ( ( ) ( ) Element of bool (Subspaces V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: PENCIL_4:7

definition

func pencil (W1,W2,k) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: PENCIL_4:def 3
(pencil (W1 : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,W2 : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (k : ( ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Subspaces_of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool (Subspaces V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: PENCIL_4:8

theorem :: PENCIL_4:9

definition

func k Pencils_of V -> ( ( ) ( ) Subset-Family of ) means :: PENCIL_4:def 4
for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) iff ex W1, W2 being ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) st
( W1 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) is ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() finite-dimensional ) Subspace of W2 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) ) & (dim W1 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) ) : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) set ) + 1 : ( ( ) ( non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = k : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & dim W2 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) set ) = k : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & X : ( ( ) ( ) set ) = pencil (W1 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) ,W2 : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) ,k : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) );

end;

theorem :: PENCIL_4:10

theorem :: PENCIL_4:11

theorem :: PENCIL_4:12

theorem :: PENCIL_4:13

theorem :: PENCIL_4:14

theorem :: PENCIL_4:15

theorem :: PENCIL_4:16

definition

func PencilSpace (V,k) -> ( ( strict ) ( strict ) TopStruct ) equals :: PENCIL_4:def 5
TopStruct(# (k : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Subspaces_of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ,(k : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Pencils_of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( strict ) TopStruct ) ;

end;

theorem :: PENCIL_4:17

theorem :: PENCIL_4:18

theorem :: PENCIL_4:19

theorem :: PENCIL_4:20

theorem :: PENCIL_4:21

begin

definition

func SubspaceSet (V,m,n) -> ( ( ) ( ) Subset-Family of ) means :: PENCIL_4:def 6
for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) in it : ( ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[: the carrier of F : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ex W being ( ( ) ( non empty V65() V102(F : ( ( ) ( ) 1-sorted ) ) V103(F : ( ( ) ( ) 1-sorted ) ) V104(F : ( ( ) ( ) 1-sorted ) ) V105(F : ( ( ) ( ) 1-sorted ) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) st
( dim W : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) : ( ( V27() ) ( V21() V22() V23() V27() finite cardinal V51() ext-real V125() ) set ) = n : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) & X : ( ( ) ( ) set ) = m : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Subspaces_of W : ( ( ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) Subspace of V : ( ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V103(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V104(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V105(F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) V112() V113() V114() finite-dimensional ) VectSp of F : ( ( non empty non degenerated V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) ( non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() ) Field) ) ) : ( ( ) ( ) set ) ) );

end;

theorem :: PENCIL_4:22

theorem :: PENCIL_4:23

theorem :: PENCIL_4:24

definition

func GrassmannSpace (V,m,n) -> ( ( strict ) ( strict ) TopStruct ) equals :: PENCIL_4:def 7
TopStruct(# (m : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Subspaces_of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ,(SubspaceSet (V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,m : ( ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) ( V6() V18([:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( ) Element of V : ( ( ) ( ) VectSpStr over F : ( ( ) ( ) 1-sorted ) ) ) )) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( strict ) TopStruct ) ;

end;

theorem :: PENCIL_4:25

theorem :: PENCIL_4:26

theorem :: PENCIL_4:27

theorem :: PENCIL_4:28

theorem :: PENCIL_4:29

begin

definition

let X be ( ( ) ( ) set ) ;

func PairSet X -> ( ( ) ( ) set ) means :: PENCIL_4:def 8
for z being ( ( ) ( ) set ) holds
( z : ( ( ) ( ) set ) in it : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) 1-sorted ) ) iff ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) 1-sorted ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) 1-sorted ) & z : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) );

end;

registration

let X be ( ( non empty ) ( non empty ) set ) ;

cluster PairSet X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

definition

let t, X be ( ( ) ( ) set ) ;

func PairSet (t,X) -> ( ( ) ( ) set ) means :: PENCIL_4:def 9
for z being ( ( ) ( ) set ) holds
( z : ( ( ) ( ) set ) in it : ( ( V6() V18([:X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) ) ) ( V6() V18([:X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) ) ) Element of bool [:[:X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ex y being ( ( ) ( ) set ) st
( y : ( ( ) ( ) set ) in X : ( ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(t : ( ( non empty ) ( non empty ) set ) ) V103(t : ( ( non empty ) ( non empty ) set ) ) V104(t : ( ( non empty ) ( non empty ) set ) ) V105(t : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over t : ( ( non empty ) ( non empty ) set ) ) & z : ( ( ) ( ) set ) = {t : ( ( non empty ) ( non empty ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) );

end;

registration

let t be ( ( ) ( ) set ) ;
let X be ( ( non empty ) ( non empty ) set ) ;

cluster PairSet (t : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -> non empty ;

end;

registration

let t be ( ( ) ( ) set ) ;
let X be ( ( non trivial ) ( non trivial ) set ) ;

cluster PairSet (t : ( ( ) ( ) set ) ,X : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( ) set ) -> non trivial ;

end;

definition

let X be ( ( ) ( ) set ) ;
let L be ( ( ) ( ) Subset-Family of ) ;

func PairSetFamily L -> ( ( ) ( ) Subset-Family of ) means :: PENCIL_4:def 10
for S being ( ( ) ( ) set ) holds
( S : ( ( ) ( ) set ) in it : ( ( V6() V18([:L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) ) ) ( V6() V18([:L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) ) ) Element of bool [:[:L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ex t being ( ( ) ( ) set ) ex l being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( t : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & l : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in L : ( ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) ( non empty V65() V102(X : ( ( non empty ) ( non empty ) set ) ) V103(X : ( ( non empty ) ( non empty ) set ) ) V104(X : ( ( non empty ) ( non empty ) set ) ) V105(X : ( ( non empty ) ( non empty ) set ) ) V112() V113() V114() finite-dimensional ) VectSpStr over X : ( ( non empty ) ( non empty ) set ) ) & S : ( ( ) ( ) set ) = PairSet (t : ( ( ) ( ) set ) ,l : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) );

end;

registration

let X be ( ( non empty ) ( non empty ) set ) ;
let L be ( ( non empty ) ( non empty ) Subset-Family of ) ;

cluster PairSetFamily L : ( ( non empty ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> non empty ;

end;

definition

let S be ( ( ) ( ) TopStruct ) ;

func VeroneseSpace S -> ( ( strict ) ( strict ) TopStruct ) equals :: PENCIL_4:def 11
TopStruct(# (PairSet the carrier of S : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(PairSetFamily the topology of S : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of bool (bool the carrier of S : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( strict ) TopStruct ) ;

end;

registration

let S be ( ( non empty ) ( non empty ) TopStruct ) ;

cluster VeroneseSpace S : ( ( non empty ) ( non empty ) TopStruct ) : ( ( strict ) ( strict ) TopStruct ) -> non empty strict ;

end;

registration

let S be ( ( non empty non void ) ( non empty non void ) TopStruct ) ;

cluster VeroneseSpace S : ( ( non empty non void ) ( non empty non void ) TopStruct ) : ( ( strict ) ( non empty strict ) TopStruct ) -> strict non void ;

end;

registration

let S be ( ( non empty non void non degenerated ) ( non empty non void non degenerated ) TopStruct ) ;

cluster VeroneseSpace S : ( ( non empty non void non degenerated ) ( non empty non void non degenerated ) TopStruct ) : ( ( strict ) ( non empty strict non void ) TopStruct ) -> strict non degenerated ;

end;

registration

let S be ( ( non empty non void with_non_trivial_blocks ) ( non empty non void with_non_trivial_blocks ) TopStruct ) ;

cluster VeroneseSpace S : ( ( non empty non void with_non_trivial_blocks ) ( non empty non void with_non_trivial_blocks ) TopStruct ) : ( ( strict ) ( non empty strict non void ) TopStruct ) -> strict with_non_trivial_blocks ;

end;

registration

let S be ( ( identifying_close_blocks ) ( identifying_close_blocks ) TopStruct ) ;

cluster VeroneseSpace S : ( ( identifying_close_blocks ) ( identifying_close_blocks ) TopStruct ) : ( ( strict ) ( strict ) TopStruct ) -> strict identifying_close_blocks ;

end;