set V5 = {1};
set E3 = {} ;
consider S1 being Function of {} ,{1};
consider W1 being ManySortedSet of ;
consider EL8 being PartFunc of {} ,REAL ;
consider VL6 being PartFunc of {1},REAL ;
set G = (((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>;
A1: ( len ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) = 7 & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 1 = {1} & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 2 = {} & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 3 = S1 & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 4 = S1 & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 5 = W1 & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 6 = EL8 & ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) . 7 = VL6 ) by FINSEQ_1:90;
then dom ((((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) = Seg 7 by FINSEQ_1:def 3;
then reconsider G = (((((<*{1}*> ^ <*{} *>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*> as GraphStruct by RELAT_1:def 18;
take G ; :: thesis: ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] )
dom G = Seg 7 by A1, FINSEQ_1:def 3;
then A2: ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & WeightSelector in dom G & ELabelSelector in dom G & VLabelSelector in dom G ) by FINSEQ_1:3;
A3: ( the_Vertices_of G = {1} & the_Edges_of G = {} & the_Source_of G = S1 & the_Target_of G = S1 & G . WeightSelector = W1 & G . ELabelSelector = EL8 & G . VLabelSelector = VL6 ) by FINSEQ_1:90;
( dom EL8 c= {} & dom VL6 c= {1} ) ;
hence ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] ) by A2, A3, Def4, Def5, Def6, GLIB_000:def 11; :: thesis: verum