:: TDGROUP semantic presentation

begin

theorem :: TDGROUP:1
for a being ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) ex b being ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) st b : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) + b : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) : ( ( ) ( V21() V29() ) Element of the carrier of G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() V125() V126() V127() ) set ) ) = a : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) ;

theorem :: TDGROUP:2
for a being ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) st a : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) + a : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) : ( ( ) ( V21() V29() ) Element of the carrier of G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() V125() V126() V127() ) set ) ) = 0. G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V21() V29() V51( G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() V125() V126() V127() ) set ) ) holds
a : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) = 0. G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V21() V29() V51( G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() V125() V126() V127() ) set ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) addLoopStr ) ;
attr IT is Two_Divisible means :: TDGROUP:def 1
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;
end;

registration
cluster G_Real : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) -> strict Fanoian Two_Divisible ;
end;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for ( ( ) ( ) addLoopStr ) ;
end;

definition
mode Two_Divisible_Group is ( ( non empty right_complementable Abelian add-associative right_zeroed Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Two_Divisible ) addLoopStr ) ;
end;

definition
mode Uniquely_Two_Divisible_Group is ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) addLoopStr ) ;
end;

theorem :: TDGROUP:3
for AG being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) holds
( AG : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() ) set ) ) = 0. AG : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V51(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = 0. AG : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V51(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V11() ) set ) ) ) ) ) ;

notation
let ADG be ( ( non empty ) ( non empty ) addLoopStr ) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;
synonym a # b for a + b;
end;

definition
let ADG be ( ( non empty ) ( non empty ) addLoopStr ) ;
func CONGRD ADG -> ( ( ) ( V1() V4([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) , the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) V5([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) , the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) means :: TDGROUP:def 2
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
( [[a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ] : ( ( ) ( ) set ) ,[c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ] : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) # d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) # c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) );
end;

definition
let ADG be ( ( non empty ) ( non empty ) addLoopStr ) ;
func AV ADG -> ( ( strict ) ( strict ) AffinStruct ) equals :: TDGROUP:def 3
 AffinStruct(# the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ,(CONGRD ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( V1() V4([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) , the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) V5([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) , the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) #) : ( ( strict ) ( strict ) AffinStruct ) ;
end;

registration
let ADG be ( ( non empty ) ( non empty ) addLoopStr ) ;
cluster AV ADG : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

theorem :: TDGROUP:4
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) holds
( the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) = the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) & the CONGR of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V1() V4([: the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) V5([: the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ,[: the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = CONGRD ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V1() V4([: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) V5([: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) ) ;

definition
let ADG be ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;
pred a,b ==> c,d means :: TDGROUP:def 4
[[a : ( ( ) ( ) set ) ,b : ( ( V6() V18([:a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) ( V1() V4([:a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(a : ( ( ) ( ) set ) ) V6() V18([:a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) Element of bool [:[:a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) ,[c : ( ( ) ( ) Element of a : ( ( ) ( ) set ) ) ,d : ( ( V6() V18([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(a : ( ( ) ( ) set ) ) V6() V18([: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the CONGR of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V1() V4([: the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) V5([: the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) ,[: the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) , the carrier of (AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed V108() well-unital V116() ) ( non empty right_complementable Abelian add-associative right_zeroed V106() V108() right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) : ( ( ) ( V11() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: TDGROUP:5
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) # d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) # c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( ) ( V11() ) set ) ) ) ;

theorem :: TDGROUP:6
ex a, b being ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) st a : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) <> b : ( ( ) ( V21() V29() ) Element of ( ( ) ( V11() V125() V126() V127() ) set ) ) ;

theorem :: TDGROUP:7
ex ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) ex a, b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:8
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:9
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, p, q, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:10
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:11
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, a9, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:12
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:13
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:14
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ==> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ;

theorem :: TDGROUP:15
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) st ex a, b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
( ex a, b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d, p, q being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is AffVect-like means :: TDGROUP:def 5
( ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d, p, q being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) );
end;

registration
cluster non empty non trivial strict AffVect-like for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode AffVect is ( ( non trivial AffVect-like ) ( non empty non trivial AffVect-like ) AffinStruct ) ;
end;

theorem :: TDGROUP:16
for AS being ( ( non empty ) ( non empty ) AffinStruct ) holds
( ( ex a, b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d, p, q being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, c being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) ) ) iff AS : ( ( non empty ) ( non empty ) AffinStruct ) is ( ( non trivial AffVect-like ) ( non empty non trivial AffVect-like ) AffVect) ) ;

theorem :: TDGROUP:17
for ADG being ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) st ex a, b being ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() ) set ) ) holds
AV ADG : ( ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) ( non empty right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible ) Uniquely_Two_Divisible_Group) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non trivial AffVect-like ) ( non empty non trivial AffVect-like ) AffVect) ;