:: PRVECT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

deffunc H1( 1-sorted ) -> set = the carrier of $1;

deffunc H2( LoopStr ) -> M6([:the carrier of $1,the carrier of $1:],the carrier of $1) = the add of $1;

deffunc H3( non empty LoopStr ) -> M6(the carrier of $1,the carrier of $1) = comp $1;

deffunc H4( LoopStr ) -> Element of the carrier of $1 = the Zero of $1;

theorem :: PRVECT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: PRVECT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds the Zero of G is_a_unity_wrt the add of G
proof end;

theorem Th4: :: PRVECT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being AbGroup holds comp G is_an_inverseOp_wrt the add of G
proof end;

Lm1: for G being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds comp G is_an_inverseOp_wrt the add of G
proof end;

theorem :: PRVECT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GS being non empty LoopStr st the add of GS is commutative & the add of GS is associative & the Zero of GS is_a_unity_wrt the add of GS & comp GS is_an_inverseOp_wrt the add of GS holds
GS is AbGroup
proof end;

Lm2: for GS being non empty LoopStr st the add of GS is commutative & the add of GS is associative holds
( GS is Abelian & GS is add-associative )
proof end;

Lm3: for GS being non empty LoopStr st the Zero of GS is_a_unity_wrt the add of GS holds
GS is right_zeroed
proof end;

Lm4: for F being Field holds the mult of F is associative
proof end;

theorem :: PRVECT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds the Zero of F is_a_unity_wrt the add of F
proof end;

theorem Th11: :: PRVECT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds 1. F is_a_unity_wrt the mult of F
proof end;

Lm5: for F being Field holds the mult of F is_distributive_wrt the add of F
proof end;

definition
let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x, y be Element of n -tuples_on D;
:: original: .:
redefine func F .: x,y -> Element of n -tuples_on D;
coherence
F .: x,y is Element of n -tuples_on D
by FINSEQ_2:140;
end;

definition
let D be non empty set ;
let F be BinOp of D;
let n be Nat;
func product F,n -> BinOp of n -tuples_on D means :Def1: :: PRVECT_1:def 1
for x, y being Element of n -tuples_on D holds it . x,y = F .: x,y;
existence
ex b1 being BinOp of n -tuples_on D st
for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y
proof end;
uniqueness
for b1, b2 being BinOp of n -tuples_on D st ( for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y ) & ( for x, y being Element of n -tuples_on D holds b2 . x,y = F .: x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines product PRVECT_1:def 1 :
for D being non empty set
for F being BinOp of D
for n being Nat
for b4 being BinOp of n -tuples_on D holds
( b4 = product F,n iff for x, y being Element of n -tuples_on D holds b4 . x,y = F .: x,y );

definition
let D be non empty set ;
let F be UnOp of D;
let n be Nat;
func product F,n -> UnOp of n -tuples_on D means :Def2: :: PRVECT_1:def 2
for x being Element of n -tuples_on D holds it . x = F * x;
existence
ex b1 being UnOp of n -tuples_on D st
for x being Element of n -tuples_on D holds b1 . x = F * x
proof end;
uniqueness
for b1, b2 being UnOp of n -tuples_on D st ( for x being Element of n -tuples_on D holds b1 . x = F * x ) & ( for x being Element of n -tuples_on D holds b2 . x = F * x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines product PRVECT_1:def 2 :
for D being non empty set
for F being UnOp of D
for n being Nat
for b4 being UnOp of n -tuples_on D holds
( b4 = product F,n iff for x being Element of n -tuples_on D holds b4 . x = F * x );

notation
let D be non empty set ;
let n be Nat;
let x be Element of D;
synonym n .--> x for D |-> n;
end;

definition
let D be non empty set ;
let n be Nat;
let x be Element of D;
:: original: .-->
redefine func n .--> x -> Element of n -tuples_on D;
correctness
coherence
x .--> is Element of n -tuples_on D
;
by FINSEQ_2:132;
end;

theorem :: PRVECT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRVECT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: PRVECT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for B being BinOp of D st B is commutative holds
product B,n is commutative
proof end;

theorem Th15: :: PRVECT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for B being BinOp of D st B is associative holds
product B,n is associative
proof end;

theorem Th16: :: PRVECT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for d being Element of D
for B being BinOp of D st d is_a_unity_wrt B holds
n .--> d is_a_unity_wrt product B,n
proof end;

theorem Th17: :: PRVECT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for B being BinOp of D
for C being UnOp of D st B has_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product C,n is_an_inverseOp_wrt product B,n
proof end;

definition
let F be non empty LoopStr ;
let n be Nat;
assume A1: ( F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable ) ;
func n -Group_over F -> strict AbGroup equals :Def3: :: PRVECT_1:def 3
LoopStr(# (n -tuples_on the carrier of F),(product the add of F,n),(n .--> the Zero of F) #);
coherence
LoopStr(# (n -tuples_on the carrier of F),(product the add of F,n),(n .--> the Zero of F) #) is strict AbGroup
proof end;
end;

:: deftheorem Def3 defines -Group_over PRVECT_1:def 3 :
for F being non empty LoopStr
for n being Nat st F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable holds
n -Group_over F = LoopStr(# (n -tuples_on the carrier of F),(product the add of F,n),(n .--> the Zero of F) #);

registration
let F be AbGroup;
let n be Nat;
cluster n -Group_over F -> strict ;
coherence
not n -Group_over F is empty
;
end;

definition
let F be Field;
let n be Nat;
func n -Mult_over F -> Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F means :Def4: :: PRVECT_1:def 4
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds it . x,v = the mult of F [;] x,v;
existence
ex b1 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F st
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the mult of F [;] x,v
proof end;
uniqueness
for b1, b2 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F st ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the mult of F [;] x,v ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b2 . x,v = the mult of F [;] x,v ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :
for F being Field
for n being Nat
for b3 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F holds
( b3 = n -Mult_over F iff for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b3 . x,v = the mult of F [;] x,v );

definition
let F be Field;
let n be Nat;
func n -VectSp_over F -> strict VectSpStr of F means :Def5: :: PRVECT_1:def 5
( LoopStr(# the carrier of it,the add of it,the Zero of it #) = n -Group_over F & the lmult of it = n -Mult_over F );
existence
ex b1 being strict VectSpStr of F st
( LoopStr(# the carrier of b1,the add of b1,the Zero of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F )
proof end;
uniqueness
for b1, b2 being strict VectSpStr of F st LoopStr(# the carrier of b1,the add of b1,the Zero of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F & LoopStr(# the carrier of b2,the add of b2,the Zero of b2 #) = n -Group_over F & the lmult of b2 = n -Mult_over F holds
b1 = b2
;
end;

:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :
for F being Field
for n being Nat
for b3 being strict VectSpStr of F holds
( b3 = n -VectSp_over F iff ( LoopStr(# the carrier of b3,the add of b3,the Zero of b3 #) = n -Group_over F & the lmult of b3 = n -Mult_over F ) );

registration
let F be Field;
let n be Nat;
cluster n -VectSp_over F -> non empty strict ;
coherence
not n -VectSp_over F is empty
proof end;
end;

theorem Th18: :: PRVECT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for H, G being BinOp of D
for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] d,(G .: t1,t2) = G .: (H [;] d,t1),(H [;] d,t2)
proof end;

definition
let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x be Element of D;
let v be Element of n -tuples_on D;
:: original: [;]
redefine func F [;] x,v -> Element of n -tuples_on D;
coherence
F [;] x,v is Element of n -tuples_on D
by FINSEQ_2:141;
end;

registration
let F be Field;
let n be Nat;
cluster n -VectSp_over F -> non empty strict VectSp-like ;
coherence
n -VectSp_over F is VectSp-like
proof end;
end;

registration
cluster non-empty non empty set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is non-empty )
proof end;
end;

definition
mode Domain-Sequence is non-empty non empty FinSequence;
end;

registration
let a be non empty Function;
cluster dom a -> non empty ;
coherence
not dom a is empty
proof end;
end;

scheme :: PRVECT_1:sch 1
NEFinSeqLambda{ F1() -> non empty FinSequence, F2( set ) -> set } :
ex p being non empty FinSequence st
( len p = len F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) )
proof end;

registration
let a be non-empty non empty Function;
let i be Element of dom a;
cluster a . i -> non empty ;
coherence
not a . i is empty
proof end;
end;

definition
let a be non-empty non empty Function;
let f be Element of product a;
let i be Element of dom a;
:: original: .
redefine func f . i -> Element of a . i;
coherence
f . i is Element of a . i
by CARD_3:18;
end;

definition
let a be non-empty non empty Function;
canceled;
canceled;
mode BinOps of a -> Function means :Def8: :: PRVECT_1:def 8
( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of a . i ) );
existence
ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is BinOp of a . i ) )
proof end;
mode UnOps of a -> Function means :Def9: :: PRVECT_1:def 9
( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of a . i ) );
existence
ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is UnOp of a . i ) )
proof end;
end;

:: deftheorem PRVECT_1:def 6 :
canceled;

:: deftheorem PRVECT_1:def 7 :
canceled;

:: deftheorem Def8 defines BinOps PRVECT_1:def 8 :
for a being non-empty non empty Function
for b2 being Function holds
( b2 is BinOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is BinOp of a . i ) ) );

:: deftheorem Def9 defines UnOps PRVECT_1:def 9 :
for a being non-empty non empty Function
for b2 being Function holds
( b2 is UnOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is UnOp of a . i ) ) );

registration
let a be Domain-Sequence;
cluster -> FinSequence-like BinOps of a;
coherence
for b1 being BinOps of a holds b1 is FinSequence-like
proof end;
cluster -> FinSequence-like UnOps of a;
coherence
for b1 being UnOps of a holds b1 is FinSequence-like
proof end;
end;

theorem Th19: :: PRVECT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for p being FinSequence holds
( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of a . i ) ) )
proof end;

theorem Th20: :: PRVECT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for p being FinSequence holds
( p is UnOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is UnOp of a . i ) ) )
proof end;

definition
let a be Domain-Sequence;
let b be BinOps of a;
let i be Element of dom a;
:: original: .
redefine func b . i -> BinOp of a . i;
coherence
b . i is BinOp of a . i
by Th19;
end;

definition
let a be Domain-Sequence;
let u be UnOps of a;
let i be Element of dom a;
:: original: .
redefine func u . i -> UnOp of a . i;
coherence
u . i is UnOp of a . i
by Th20;
end;

definition
let F be non empty functional set ;
let u be UnOp of F;
let f be Element of F;
:: original: .
redefine func u . f -> Element of F;
coherence
u . f is Element of F
proof end;
end;

theorem :: PRVECT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for d, d' being UnOp of product a st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d' . f) . i ) holds
d = d'
proof end;

theorem Th22: :: PRVECT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
proof end;

definition
let a be Domain-Sequence;
let u be UnOps of a;
:: original: Frege
redefine func Frege u -> UnOp of product a;
coherence
Frege u is UnOp of product a
proof end;
end;

theorem Th23: :: PRVECT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for u being UnOps of a
for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
proof end;

definition
let F be non empty functional set ;
let b be BinOp of F;
let f, g be Element of F;
:: original: .
redefine func b . f,g -> Element of F;
coherence
b . f,g is Element of F
proof end;
end;

theorem Th24: :: PRVECT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for d, d' being BinOp of product a st ( for f, g being Element of product a
for i being Element of dom a holds (d . f,g) . i = (d' . f,g) . i ) holds
d = d'
proof end;

definition
let a be Domain-Sequence;
let b be BinOps of a;
func [:b:] -> BinOp of product a means :Def10: :: PRVECT_1:def 10
for f, g being Element of product a
for i being Element of dom a holds (it . f,g) . i = (b . i) . (f . i),(g . i);
existence
ex b1 being BinOp of product a st
for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i)
proof end;
uniqueness
for b1, b2 being BinOp of product a st ( for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i) ) & ( for f, g being Element of product a
for i being Element of dom a holds (b2 . f,g) . i = (b . i) . (f . i),(g . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines [: PRVECT_1:def 10 :
for a being Domain-Sequence
for b being BinOps of a
for b3 being BinOp of product a holds
( b3 = [:b:] iff for f, g being Element of product a
for i being Element of dom a holds (b3 . f,g) . i = (b . i) . (f . i),(g . i) );

theorem Th25: :: PRVECT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative
proof end;

theorem Th26: :: PRVECT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative
proof end;

theorem Th27: :: PRVECT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for b being BinOps of a
for f being Element of product a st ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) holds
f is_a_unity_wrt [:b:]
proof end;

theorem Th28: :: PRVECT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Domain-Sequence
for b being BinOps of a
for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i has_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
proof end;

definition
let F be Relation;
attr F is AbGroup-yielding means :Def11: :: PRVECT_1:def 11
for x being set st x in rng F holds
x is AbGroup;
end;

:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :
for F being Relation holds
( F is AbGroup-yielding iff for x being set st x in rng F holds
x is AbGroup );

registration
cluster non empty AbGroup-yielding set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is AbGroup-yielding )
proof end;
end;

definition
mode Group-Sequence is non empty AbGroup-yielding FinSequence;
end;

definition
let g be Group-Sequence;
let i be Element of dom g;
:: original: .
redefine func g . i -> AbGroup;
coherence
g . i is AbGroup
proof end;
end;

definition
let g be Group-Sequence;
func carr g -> Domain-Sequence means :Def12: :: PRVECT_1:def 12
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
existence
ex b1 being Domain-Sequence st
( len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) )
proof end;
uniqueness
for b1, b2 being Domain-Sequence st len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) & len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines carr PRVECT_1:def 12 :
for g being Group-Sequence
for b2 being Domain-Sequence holds
( b2 = carr g iff ( len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) ) );

definition
let g be Group-Sequence;
let i be Element of dom (carr g);
:: original: .
redefine func g . i -> AbGroup;
coherence
g . i is AbGroup
proof end;
end;

definition
let g be Group-Sequence;
func addop g -> BinOps of carr g means :Def13: :: PRVECT_1:def 13
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the add of (g . i) ) );
existence
ex b1 being BinOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the add of (g . i) ) )
proof end;
uniqueness
for b1, b2 being BinOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the add of (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the add of (g . i) ) holds
b1 = b2
proof end;
func complop g -> UnOps of carr g means :Def14: :: PRVECT_1:def 14
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );
existence
ex b1 being UnOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) )
proof end;
uniqueness
for b1, b2 being UnOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) holds
b1 = b2
proof end;
func zeros g -> Element of product (carr g) means :Def15: :: PRVECT_1:def 15
for i being Element of dom (carr g) holds it . i = the Zero of (g . i);
existence
ex b1 being Element of product (carr g) st
for i being Element of dom (carr g) holds b1 . i = the Zero of (g . i)
proof end;
uniqueness
for b1, b2 being Element of product (carr g) st ( for i being Element of dom (carr g) holds b1 . i = the Zero of (g . i) ) & ( for i being Element of dom (carr g) holds b2 . i = the Zero of (g . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines addop PRVECT_1:def 13 :
for g being Group-Sequence
for b2 being BinOps of carr g holds
( b2 = addop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the add of (g . i) ) ) );

:: deftheorem Def14 defines complop PRVECT_1:def 14 :
for g being Group-Sequence
for b2 being UnOps of carr g holds
( b2 = complop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) ) );

:: deftheorem Def15 defines zeros PRVECT_1:def 15 :
for g being Group-Sequence
for b2 being Element of product (carr g) holds
( b2 = zeros g iff for i being Element of dom (carr g) holds b2 . i = the Zero of (g . i) );

definition
let G be Group-Sequence;
func product G -> strict AbGroup equals :: PRVECT_1:def 16
LoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence
LoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup
proof end;
end;

:: deftheorem defines product PRVECT_1:def 16 :
for G being Group-Sequence holds product G = LoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);