:: PRVECT_1 semantic presentation

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

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

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

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

theorem Th1: :: PRVECT_1:1
canceled;

theorem Th2: :: PRVECT_1:2
canceled;

theorem Th3: :: PRVECT_1:3
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds the Zero of b1 is_a_unity_wrt the add of b1
proof end;

theorem Th4: :: PRVECT_1:4
for b1 being AbGroup holds comp b1 is_an_inverseOp_wrt the add of b1
proof end;

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

theorem Th5: :: PRVECT_1:5
for b1 being non empty LoopStr st the add of b1 is commutative & the add of b1 is associative & the Zero of b1 is_a_unity_wrt the add of b1 & comp b1 is_an_inverseOp_wrt the add of b1 holds
b1 is AbGroup
proof end;

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

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

Lemma6: for b1 being Field holds the mult of b1 is associative
proof end;

theorem Th6: :: PRVECT_1:6
canceled;

theorem Th7: :: PRVECT_1:7
canceled;

theorem Th8: :: PRVECT_1:8
canceled;

theorem Th9: :: PRVECT_1:9
canceled;

theorem Th10: :: PRVECT_1:10
for b1 being Field holds the Zero of b1 is_a_unity_wrt the add of b1
proof end;

theorem Th11: :: PRVECT_1:11
for b1 being Field holds 1. b1 is_a_unity_wrt the mult of b1
proof end;

Lemma8: for b1 being Field holds the mult of b1 is_distributive_wrt the add of b1
proof end;

definition
let c1 be non empty set ;
let c2 be Nat;
let c3 be BinOp of c1;
let c4, c5 be Element of c2 -tuples_on c1;
redefine func .: as c3 .: c4,c5 -> Element of a2 -tuples_on a1;
coherence
c3 .: c4,c5 is Element of c2 -tuples_on c1 by FINSEQ_2:140;
end;

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
let c3 be Nat;
func product c2,c3 -> BinOp of a3 -tuples_on a1 means :Def1: :: PRVECT_1:def 1
for b1, b2 being Element of a3 -tuples_on a1 holds a4 . b1,b2 = a2 .: b1,b2;
existence
ex b1 being BinOp of c3 -tuples_on c1 st
for b2, b3 being Element of c3 -tuples_on c1 holds b1 . b2,b3 = c2 .: b2,b3
proof end;
uniqueness
for b1, b2 being BinOp of c3 -tuples_on c1 st ( for b3, b4 being Element of c3 -tuples_on c1 holds b1 . b3,b4 = c2 .: b3,b4 ) & ( for b3, b4 being Element of c3 -tuples_on c1 holds b2 . b3,b4 = c2 .: b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines product PRVECT_1:def 1 :
for b1 being non empty set
for b2 being BinOp of b1
for b3 being Nat
for b4 being BinOp of b3 -tuples_on b1 holds
( b4 = product b2,b3 iff for b5, b6 being Element of b3 -tuples_on b1 holds b4 . b5,b6 = b2 .: b5,b6 );

definition
let c1 be non empty set ;
let c2 be UnOp of c1;
let c3 be Nat;
func product c2,c3 -> UnOp of a3 -tuples_on a1 means :Def2: :: PRVECT_1:def 2
for b1 being Element of a3 -tuples_on a1 holds a4 . b1 = a2 * b1;
existence
ex b1 being UnOp of c3 -tuples_on c1 st
for b2 being Element of c3 -tuples_on c1 holds b1 . b2 = c2 * b2
proof end;
uniqueness
for b1, b2 being UnOp of c3 -tuples_on c1 st ( for b3 being Element of c3 -tuples_on c1 holds b1 . b3 = c2 * b3 ) & ( for b3 being Element of c3 -tuples_on c1 holds b2 . b3 = c2 * b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines product PRVECT_1:def 2 :
for b1 being non empty set
for b2 being UnOp of b1
for b3 being Nat
for b4 being UnOp of b3 -tuples_on b1 holds
( b4 = product b2,b3 iff for b5 being Element of b3 -tuples_on b1 holds b4 . b5 = b2 * b5 );

notation
let c1 be non empty set ;
let c2 be Nat;
let c3 be Element of c1;
synonym c2 .--> c3 for c1 |-> c2;
end;

definition
let c1 be non empty set ;
let c2 be Nat;
let c3 be Element of c1;
redefine func .--> as c2 .--> c3 -> Element of a2 -tuples_on a1;
correctness
coherence
c3 .--> is Element of c2 -tuples_on c1;
by FINSEQ_2:132;
end;

theorem Th12: :: PRVECT_1:12
canceled;

theorem Th13: :: PRVECT_1:13
canceled;

theorem Th14: :: PRVECT_1:14
for b1 being Nat
for b2 being non empty set
for b3 being BinOp of b2 st b3 is commutative holds
product b3,b1 is commutative
proof end;

theorem Th15: :: PRVECT_1:15
for b1 being Nat
for b2 being non empty set
for b3 being BinOp of b2 st b3 is associative holds
product b3,b1 is associative
proof end;

theorem Th16: :: PRVECT_1:16
for b1 being Nat
for b2 being non empty set
for b3 being Element of b2
for b4 being BinOp of b2 st b3 is_a_unity_wrt b4 holds
b1 .--> b3 is_a_unity_wrt product b4,b1
proof end;

theorem Th17: :: PRVECT_1:17
for b1 being Nat
for b2 being non empty set
for b3 being BinOp of b2
for b4 being UnOp of b2 st b3 has_a_unity & b3 is associative & b4 is_an_inverseOp_wrt b3 holds
product b4,b1 is_an_inverseOp_wrt product b3,b1
proof end;

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

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

registration
let c1 be AbGroup;
let c2 be Nat;
cluster a2 -Group_over a1 -> strict ;
coherence
not c2 -Group_over c1 is empty ;
end;

definition
let c1 be Field;
let c2 be Nat;
func c2 -Mult_over c1 -> Function of [:the carrier of a1,(a2 -tuples_on the carrier of a1):],a2 -tuples_on the carrier of a1 means :Def4: :: PRVECT_1:def 4
for b1 being Element of a1
for b2 being Element of a2 -tuples_on the carrier of a1 holds a3 . b1,b2 = the mult of a1 [;] b1,b2;
existence
ex b1 being Function of [:the carrier of c1,(c2 -tuples_on the carrier of c1):],c2 -tuples_on the carrier of c1 st
for b2 being Element of c1
for b3 being Element of c2 -tuples_on the carrier of c1 holds b1 . b2,b3 = the mult of c1 [;] b2,b3
proof end;
uniqueness
for b1, b2 being Function of [:the carrier of c1,(c2 -tuples_on the carrier of c1):],c2 -tuples_on the carrier of c1 st ( for b3 being Element of c1
for b4 being Element of c2 -tuples_on the carrier of c1 holds b1 . b3,b4 = the mult of c1 [;] b3,b4 ) & ( for b3 being Element of c1
for b4 being Element of c2 -tuples_on the carrier of c1 holds b2 . b3,b4 = the mult of c1 [;] b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :
for b1 being Field
for b2 being Nat
for b3 being Function of [:the carrier of b1,(b2 -tuples_on the carrier of b1):],b2 -tuples_on the carrier of b1 holds
( b3 = b2 -Mult_over b1 iff for b4 being Element of b1
for b5 being Element of b2 -tuples_on the carrier of b1 holds b3 . b4,b5 = the mult of b1 [;] b4,b5 );

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

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

registration
let c1 be Field;
let c2 be Nat;
cluster a2 -VectSp_over a1 -> non empty strict ;
coherence
not c2 -VectSp_over c1 is empty
proof end;
end;

theorem Th18: :: PRVECT_1:18
for b1 being Nat
for b2 being non empty set
for b3, b4 being BinOp of b2
for b5 being Element of b2
for b6, b7 being Element of b1 -tuples_on b2 st b3 is_distributive_wrt b4 holds
b3 [;] b5,(b4 .: b6,b7) = b4 .: (b3 [;] b5,b6),(b3 [;] b5,b7)
proof end;

definition
let c1 be non empty set ;
let c2 be Nat;
let c3 be BinOp of c1;
let c4 be Element of c1;
let c5 be Element of c2 -tuples_on c1;
redefine func [;] as c3 [;] c4,c5 -> Element of a2 -tuples_on a1;
coherence
c3 [;] c4,c5 is Element of c2 -tuples_on c1 by FINSEQ_2:141;
end;

registration
let c1 be Field;
let c2 be Nat;
cluster a2 -VectSp_over a1 -> non empty strict VectSp-like ;
coherence
c2 -VectSp_over c1 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 c1 be non empty Function;
cluster dom a1 -> non empty ;
coherence
not dom c1 is empty
proof end;
end;

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

registration
let c1 be non-empty non empty Function;
let c2 be Element of dom c1;
cluster a1 . a2 -> non empty ;
coherence
not c1 . c2 is empty
proof end;
end;

definition
let c1 be non-empty non empty Function;
let c2 be Element of product c1;
let c3 be Element of dom c1;
redefine func . as c2 . c3 -> Element of a1 . a3;
coherence
c2 . c3 is Element of c1 . c3 by CARD_3:18;
end;

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

:: deftheorem Def6 PRVECT_1:def 6 :
canceled;

:: deftheorem Def7 PRVECT_1:def 7 :
canceled;

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

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

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

theorem Th19: :: PRVECT_1:19
for b1 being Domain-Sequence
for b2 being FinSequence holds
( b2 is BinOps of b1 iff ( len b2 = len b1 & ( for b3 being Element of dom b1 holds b2 . b3 is BinOp of b1 . b3 ) ) )
proof end;

theorem Th20: :: PRVECT_1:20
for b1 being Domain-Sequence
for b2 being FinSequence holds
( b2 is UnOps of b1 iff ( len b2 = len b1 & ( for b3 being Element of dom b1 holds b2 . b3 is UnOp of b1 . b3 ) ) )
proof end;

definition
let c1 be Domain-Sequence;
let c2 be BinOps of c1;
let c3 be Element of dom c1;
redefine func . as c2 . c3 -> BinOp of a1 . a3;
coherence
c2 . c3 is BinOp of c1 . c3 by Th19;
end;

definition
let c1 be Domain-Sequence;
let c2 be UnOps of c1;
let c3 be Element of dom c1;
redefine func . as c2 . c3 -> UnOp of a1 . a3;
coherence
c2 . c3 is UnOp of c1 . c3 by Th20;
end;

definition
let c1 be non empty functional set ;
let c2 be UnOp of c1;
let c3 be Element of c1;
redefine func . as c2 . c3 -> Element of a1;
coherence
c2 . c3 is Element of c1
proof end;
end;

theorem Th21: :: PRVECT_1:21
for b1 being Domain-Sequence
for b2, b3 being UnOp of product b1 st ( for b4 being Element of product b1
for b5 being Element of dom b1 holds (b2 . b4) . b5 = (b3 . b4) . b5 ) holds
b2 = b3
proof end;

theorem Th22: :: PRVECT_1:22
for b1 being Domain-Sequence
for b2 being UnOps of b1 holds
( doms b2 = b1 & product (rngs b2) c= product b1 )
proof end;

definition
let c1 be Domain-Sequence;
let c2 be UnOps of c1;
redefine func Frege as Frege c2 -> UnOp of product a1;
coherence
Frege c2 is UnOp of product c1
proof end;
end;

theorem Th23: :: PRVECT_1:23
for b1 being Domain-Sequence
for b2 being UnOps of b1
for b3 being Element of product b1
for b4 being Element of dom b1 holds ((Frege b2) . b3) . b4 = (b2 . b4) . (b3 . b4)
proof end;

definition
let c1 be non empty functional set ;
let c2 be BinOp of c1;
let c3, c4 be Element of c1;
redefine func . as c2 . c3,c4 -> Element of a1;
coherence
c2 . c3,c4 is Element of c1
proof end;
end;

theorem Th24: :: PRVECT_1:24
for b1 being Domain-Sequence
for b2, b3 being BinOp of product b1 st ( for b4, b5 being Element of product b1
for b6 being Element of dom b1 holds (b2 . b4,b5) . b6 = (b3 . b4,b5) . b6 ) holds
b2 = b3
proof end;

definition
let c1 be Domain-Sequence;
let c2 be BinOps of c1;
func [:c2:] -> BinOp of product a1 means :Def10: :: PRVECT_1:def 10
for b1, b2 being Element of product a1
for b3 being Element of dom a1 holds (a3 . b1,b2) . b3 = (a2 . b3) . (b1 . b3),(b2 . b3);
existence
ex b1 being BinOp of product c1 st
for b2, b3 being Element of product c1
for b4 being Element of dom c1 holds (b1 . b2,b3) . b4 = (c2 . b4) . (b2 . b4),(b3 . b4)
proof end;
uniqueness
for b1, b2 being BinOp of product c1 st ( for b3, b4 being Element of product c1
for b5 being Element of dom c1 holds (b1 . b3,b4) . b5 = (c2 . b5) . (b3 . b5),(b4 . b5) ) & ( for b3, b4 being Element of product c1
for b5 being Element of dom c1 holds (b2 . b3,b4) . b5 = (c2 . b5) . (b3 . b5),(b4 . b5) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines [: PRVECT_1:def 10 :
for b1 being Domain-Sequence
for b2 being BinOps of b1
for b3 being BinOp of product b1 holds
( b3 = [:b2:] iff for b4, b5 being Element of product b1
for b6 being Element of dom b1 holds (b3 . b4,b5) . b6 = (b2 . b6) . (b4 . b6),(b5 . b6) );

theorem Th25: :: PRVECT_1:25
for b1 being Domain-Sequence
for b2 being BinOps of b1 st ( for b3 being Element of dom b1 holds b2 . b3 is commutative ) holds
[:b2:] is commutative
proof end;

theorem Th26: :: PRVECT_1:26
for b1 being Domain-Sequence
for b2 being BinOps of b1 st ( for b3 being Element of dom b1 holds b2 . b3 is associative ) holds
[:b2:] is associative
proof end;

theorem Th27: :: PRVECT_1:27
for b1 being Domain-Sequence
for b2 being BinOps of b1
for b3 being Element of product b1 st ( for b4 being Element of dom b1 holds b3 . b4 is_a_unity_wrt b2 . b4 ) holds
b3 is_a_unity_wrt [:b2:]
proof end;

theorem Th28: :: PRVECT_1:28
for b1 being Domain-Sequence
for b2 being BinOps of b1
for b3 being UnOps of b1 st ( for b4 being Element of dom b1 holds
( b3 . b4 is_an_inverseOp_wrt b2 . b4 & b2 . b4 has_a_unity ) ) holds
Frege b3 is_an_inverseOp_wrt [:b2:]
proof end;

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

:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :
for b1 being Relation holds
( b1 is AbGroup-yielding iff for b2 being set st b2 in rng b1 holds
b2 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 c1 be Group-Sequence;
let c2 be Element of dom c1;
redefine func . as c1 . c2 -> AbGroup;
coherence
c1 . c2 is AbGroup
proof end;
end;

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

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

definition
let c1 be Group-Sequence;
let c2 be Element of dom (carr c1);
redefine func . as c1 . c2 -> AbGroup;
coherence
c1 . c2 is AbGroup
proof end;
end;

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

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

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

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

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

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