:: by Anna Lango and Grzegorz Bancerek

::

:: Received December 29, 1992

:: Copyright (c) 1992-2017 Association of Mizar Users

deffunc H

deffunc H

deffunc H

deffunc H

theorem Th1: :: PRVECT_1:1

for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds 0. G is_a_unity_wrt the addF of G

proof end;

Lm1: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp G is_an_inverseOp_wrt the addF of G

proof end;

theorem :: PRVECT_1:3

for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative & 0. GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS holds

GS is AbGroup

GS is AbGroup

proof end;

Lm2: for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative holds

( GS is Abelian & GS is add-associative )

;

Lm3: for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds

GS is right_zeroed

by BINOP_1:3;

Lm4: for F being Field holds the multF of F is associative

proof end;

Lm5: for F being Field holds the multF of F is_distributive_wrt the addF 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:120;

end;
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:120;

definition

let D be non empty set ;

let F be BinOp of D;

let n be Nat;

ex b_{1} being BinOp of (n -tuples_on D) st

for x, y being Element of n -tuples_on D holds b_{1} . (x,y) = F .: (x,y)

for b_{1}, b_{2} being BinOp of (n -tuples_on D) st ( for x, y being Element of n -tuples_on D holds b_{1} . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds b_{2} . (x,y) = F .: (x,y) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of n -tuples_on D holds it . (x,y) = F .: (x,y);

ex b

for x, y being Element of n -tuples_on D holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being BinOp of (n -tuples_on D) holds

( b_{4} = product (F,n) iff for x, y being Element of n -tuples_on D holds b_{4} . (x,y) = F .: (x,y) );

for D being non empty set

for F being BinOp of D

for n being Nat

for b

( b

definition

let D be non empty set ;

let F be UnOp of D;

let n be Nat;

ex b_{1} being UnOp of (n -tuples_on D) st

for x being Element of n -tuples_on D holds b_{1} . x = F * x

for b_{1}, b_{2} being UnOp of (n -tuples_on D) st ( for x being Element of n -tuples_on D holds b_{1} . x = F * x ) & ( for x being Element of n -tuples_on D holds b_{2} . x = F * x ) holds

b_{1} = b_{2}

end;
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 for x being Element of n -tuples_on D holds it . x = F * x;

ex b

for x being Element of n -tuples_on D holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being UnOp of (n -tuples_on D) holds

( b_{4} = product (F,n) iff for x being Element of n -tuples_on D holds b_{4} . x = F * x );

for D being non empty set

for F being UnOp of D

for n being Nat

for b

( b

theorem Th6: :: PRVECT_1:6

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

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 Th7: :: PRVECT_1:7

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

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 Th8: :: PRVECT_1:8

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)

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 Th9: :: PRVECT_1:9

for n being Nat

for D being non empty set

for B being BinOp of D

for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds

product (C,n) is_an_inverseOp_wrt product (B,n)

for D being non empty set

for B being BinOp of D

for C being UnOp of D st B is having_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 addLoopStr ;

let n be Nat;

assume A1: ( F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable ) ;

addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup

end;
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

addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

coherence addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup

proof end;

:: deftheorem Def3 defines -Group_over PRVECT_1:def 3 :

for F being non empty addLoopStr

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 = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

for F being non empty addLoopStr

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 = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

definition

let F be Field;

let n be Nat;

ex b_{1} 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 b_{1} . (x,v) = the multF of F [;] (x,v)

for b_{1}, b_{2} 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 b_{1} . (x,v) = the multF of F [;] (x,v) ) & ( for x being Element of F

for v being Element of n -tuples_on the carrier of F holds b_{2} . (x,v) = the multF of F [;] (x,v) ) holds

b_{1} = b_{2}

end;
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 multF of F [;] (x,v);

existence for x being Element of F

for v being Element of n -tuples_on the carrier of F holds it . (x,v) = the multF of F [;] (x,v);

ex b

for x being Element of F

for v being Element of n -tuples_on the carrier of F holds b

proof end;

uniqueness for b

for v being Element of n -tuples_on the carrier of F holds b

for v being Element of n -tuples_on the carrier of F holds b

b

proof end;

:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :

for F being Field

for n being Nat

for b_{3} being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) holds

( b_{3} = n -Mult_over F iff for x being Element of F

for v being Element of n -tuples_on the carrier of F holds b_{3} . (x,v) = the multF of F [;] (x,v) );

for F being Field

for n being Nat

for b

( b

for v being Element of n -tuples_on the carrier of F holds b

definition

let F be Field;

let n be Nat;

ex b_{1} being strict ModuleStr over F st

( addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = n -Group_over F & the lmult of b_{1} = n -Mult_over F )

for b_{1}, b_{2} being strict ModuleStr over F st addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = n -Group_over F & the lmult of b_{1} = n -Mult_over F & addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = n -Group_over F & the lmult of b_{2} = n -Mult_over F holds

b_{1} = b_{2}
;

end;
let n be Nat;

func n -VectSp_over F -> strict ModuleStr over F means :Def5: :: PRVECT_1:def 5

( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = n -Group_over F & the lmult of it = n -Mult_over F );

existence ( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = n -Group_over F & the lmult of it = n -Mult_over F );

ex b

( addLoopStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :

for F being Field

for n being Nat

for b_{3} being strict ModuleStr over F holds

( b_{3} = n -VectSp_over F iff ( addLoopStr(# the carrier of b_{3}, the addF of b_{3}, the ZeroF of b_{3} #) = n -Group_over F & the lmult of b_{3} = n -Mult_over F ) );

for F being Field

for n being Nat

for b

( b

theorem Th10: :: PRVECT_1:10

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)))

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:121;

end;
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:121;

registration

let F be Field;

let n be Nat;

( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital )

end;
let n be Nat;

cluster n -VectSp_over F -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital )

proof end;

scheme :: PRVECT_1:sch 1

NEFinSeqLambda{ F_{1}() -> non empty FinSequence, F_{2}( set ) -> set } :

NEFinSeqLambda{ F

ex p being non empty FinSequence st

( len p = len F_{1}() & ( for i being Element of dom F_{1}() holds p . i = F_{2}(i) ) )

( len p = len F

proof 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:9;

end;
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:9;

definition

let a be non-empty non empty Function;

ex b_{1} being Function st

( dom b_{1} = dom a & ( for i being Element of dom a holds b_{1} . i is BinOp of (a . i) ) )

ex b_{1} being Function st

( dom b_{1} = dom a & ( for i being Element of dom a holds b_{1} . i is UnOp of (a . i) ) )

end;
mode BinOps of a -> Function means :Def6: :: PRVECT_1:def 6

( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of (a . i) ) );

existence ( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of (a . i) ) );

ex b

( dom b

proof end;

mode UnOps of a -> Function means :Def7: :: PRVECT_1:def 7

( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of (a . i) ) );

existence ( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of (a . i) ) );

ex b

( dom b

proof end;

:: deftheorem Def6 defines BinOps PRVECT_1:def 6 :

for a being non-empty non empty Function

for b_{2} being Function holds

( b_{2} is BinOps of a iff ( dom b_{2} = dom a & ( for i being Element of dom a holds b_{2} . i is BinOp of (a . i) ) ) );

for a being non-empty non empty Function

for b

( b

:: deftheorem Def7 defines UnOps PRVECT_1:def 7 :

for a being non-empty non empty Function

for b_{2} being Function holds

( b_{2} is UnOps of a iff ( dom b_{2} = dom a & ( for i being Element of dom a holds b_{2} . i is UnOp of (a . i) ) ) );

for a being non-empty non empty Function

for b

( b

registration

let a be Domain-Sequence;

coherence

for b_{1} being BinOps of a holds b_{1} is FinSequence-like

for b_{1} being UnOps of a holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let a be Domain-Sequence;

coherence

for b_{1} being BinOps of a holds b_{1} is Function-yielding

for b_{1} being UnOps of a holds b_{1} is Function-yielding

end;
coherence

for b

proof end;

coherence for b

proof end;

theorem Th11: :: PRVECT_1:11

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) ) ) )

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 Th12: :: PRVECT_1:12

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) ) ) )

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 Th11;

end;
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 Th11;

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 Th12;

end;
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 Th12;

theorem :: PRVECT_1:13

for a being Domain-Sequence

for d, d9 being UnOp of (product a) st ( for f being Element of product a

for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds

d = d9

for d, d9 being UnOp of (product a) st ( for f being Element of product a

for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds

d = d9

proof end;

theorem Th14: :: PRVECT_1:14

for a being Domain-Sequence

for u being UnOps of a holds

( doms u = a & product (rngs u) c= product a )

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)

end;
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;

theorem Th15: :: PRVECT_1:15

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)

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;

theorem Th16: :: PRVECT_1:16

for a being Domain-Sequence

for d, d9 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 = (d9 . (f,g)) . i ) holds

d = d9

for d, d9 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 = (d9 . (f,g)) . i ) holds

d = d9

proof end;

definition

let a be Domain-Sequence;

let b be BinOps of a;

ex b_{1} being BinOp of (product a) st

for f, g being Element of product a

for i being Element of dom a holds (b_{1} . (f,g)) . i = (b . i) . ((f . i),(g . i))

for b_{1}, b_{2} being BinOp of (product a) st ( for f, g being Element of product a

for i being Element of dom a holds (b_{1} . (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 (b_{2} . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) holds

b_{1} = b_{2}

end;
let b be BinOps of a;

func [:b:] -> BinOp of (product a) means :Def8: :: PRVECT_1:def 8

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 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));

ex b

for f, g being Element of product a

for i being Element of dom a holds (b

proof end;

uniqueness for b

for i being Element of dom a holds (b

for i being Element of dom a holds (b

b

proof end;

:: deftheorem Def8 defines [: PRVECT_1:def 8 :

for a being Domain-Sequence

for b being BinOps of a

for b_{3} being BinOp of (product a) holds

( b_{3} = [:b:] iff for f, g being Element of product a

for i being Element of dom a holds (b_{3} . (f,g)) . i = (b . i) . ((f . i),(g . i)) );

for a being Domain-Sequence

for b being BinOps of a

for b

( b

for i being Element of dom a holds (b

theorem Th17: :: PRVECT_1:17

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

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 Th18: :: PRVECT_1:18

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

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 Th19: :: PRVECT_1:19

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:]

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 Th20: :: PRVECT_1:20

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 is having_a_unity ) ) holds

Frege u is_an_inverseOp_wrt [:b:]

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 is having_a_unity ) ) holds

Frege u is_an_inverseOp_wrt [:b:]

proof end;

definition

let F be Relation;

end;
attr F is non-empty-addLoopStr-yielding means :DefAA: :: PRVECT_1:def 9

for x being set st x in rng F holds

x is non empty addLoopStr ;

for x being set st x in rng F holds

x is non empty addLoopStr ;

attr F is AbGroup-yielding means :Def9: :: PRVECT_1:def 10

for x being set st x in rng F holds

x is AbGroup;

for x being set st x in rng F holds

x is AbGroup;

:: deftheorem DefAA defines non-empty-addLoopStr-yielding PRVECT_1:def 9 :

for F being Relation holds

( F is non-empty-addLoopStr-yielding iff for x being set st x in rng F holds

x is non empty addLoopStr );

for F being Relation holds

( F is non-empty-addLoopStr-yielding iff for x being set st x in rng F holds

x is non empty addLoopStr );

:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def 10 :

for F being Relation holds

( F is AbGroup-yielding iff for x being set st x in rng F holds

x is AbGroup );

for F being Relation holds

( F is AbGroup-yielding iff for x being set st x in rng F holds

x is AbGroup );

registration

coherence

for b_{1} being Relation st b_{1} is AbGroup-yielding holds

b_{1} is non-empty-addLoopStr-yielding
;

end;
for b

b

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is AbGroup-yielding )
end;

cluster Relation-like NAT -defined Function-like non empty V39() countable FinSequence-like FinSubsequence-like AbGroup-yielding for set ;

existence ex b

( not b

proof end;

definition

let g be non empty non-empty-addLoopStr-yielding FinSequence;

let i be Element of dom g;

:: original: .

redefine func g . i -> non empty addLoopStr ;

coherence

g . i is non empty addLoopStr

end;
let i be Element of dom g;

:: original: .

redefine func g . i -> non empty addLoopStr ;

coherence

g . i is non empty addLoopStr

proof 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

end;
let i be Element of dom g;

:: original: .

redefine func g . i -> AbGroup;

coherence

g . i is AbGroup

proof end;

definition

let g be non empty non-empty-addLoopStr-yielding FinSequence;

ex b_{1} being Domain-Sequence st

( len b_{1} = len g & ( for j being Element of dom g holds b_{1} . j = the carrier of (g . j) ) )

for b_{1}, b_{2} being Domain-Sequence st len b_{1} = len g & ( for j being Element of dom g holds b_{1} . j = the carrier of (g . j) ) & len b_{2} = len g & ( for j being Element of dom g holds b_{2} . j = the carrier of (g . j) ) holds

b_{1} = b_{2}

end;
func carr g -> Domain-Sequence means :Def10: :: PRVECT_1:def 11

( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );

existence ( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines carr PRVECT_1:def 11 :

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b_{2} being Domain-Sequence holds

( b_{2} = carr g iff ( len b_{2} = len g & ( for j being Element of dom g holds b_{2} . j = the carrier of (g . j) ) ) );

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b

( b

definition

let g be non empty non-empty-addLoopStr-yielding FinSequence;

let i be Element of dom (carr g);

:: original: .

redefine func g . i -> non empty addLoopStr ;

coherence

g . i is non empty addLoopStr

end;
let i be Element of dom (carr g);

:: original: .

redefine func g . i -> non empty addLoopStr ;

coherence

g . i is non empty addLoopStr

proof end;

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

end;
let i be Element of dom (carr g);

:: original: .

redefine func g . i -> AbGroup;

coherence

g . i is AbGroup

proof end;

definition

let g be non empty non-empty-addLoopStr-yielding FinSequence;

ex b_{1} being BinOps of carr g st

( len b_{1} = len (carr g) & ( for i being Element of dom (carr g) holds b_{1} . i = the addF of (g . i) ) )

for b_{1}, b_{2} being BinOps of carr g st len b_{1} = len (carr g) & ( for i being Element of dom (carr g) holds b_{1} . i = the addF of (g . i) ) & len b_{2} = len (carr g) & ( for i being Element of dom (carr g) holds b_{2} . i = the addF of (g . i) ) holds

b_{1} = b_{2}

end;
func addop g -> BinOps of carr g means :Def11: :: PRVECT_1:def 12

( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF of (g . i) ) );

existence ( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF of (g . i) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines addop PRVECT_1:def 12 :

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b_{2} being BinOps of carr g holds

( b_{2} = addop g iff ( len b_{2} = len (carr g) & ( for i being Element of dom (carr g) holds b_{2} . i = the addF of (g . i) ) ) );

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b

( b

definition

let g be non empty non-empty-addLoopStr-yielding FinSequence;

ex b_{1} being UnOps of carr g st

( len b_{1} = len (carr g) & ( for i being Element of dom (carr g) holds b_{1} . i = comp (g . i) ) )

for b_{1}, b_{2} being UnOps of carr g st len b_{1} = len (carr g) & ( for i being Element of dom (carr g) holds b_{1} . i = comp (g . i) ) & len b_{2} = len (carr g) & ( for i being Element of dom (carr g) holds b_{2} . i = comp (g . i) ) holds

b_{1} = b_{2}

ex b_{1} being Element of product (carr g) st

for i being Element of dom (carr g) holds b_{1} . i = 0. (g . i)

for b_{1}, b_{2} being Element of product (carr g) st ( for i being Element of dom (carr g) holds b_{1} . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds b_{2} . i = 0. (g . i) ) holds

b_{1} = b_{2}

end;
func complop g -> UnOps of carr g means :Def12: :: PRVECT_1:def 13

( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );

existence ( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

func zeros g -> Element of product (carr g) means :Def13: :: PRVECT_1:def 14

for i being Element of dom (carr g) holds it . i = 0. (g . i);

existence for i being Element of dom (carr g) holds it . i = 0. (g . i);

ex b

for i being Element of dom (carr g) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines complop PRVECT_1:def 13 :

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b_{2} being UnOps of carr g holds

( b_{2} = complop g iff ( len b_{2} = len (carr g) & ( for i being Element of dom (carr g) holds b_{2} . i = comp (g . i) ) ) );

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b

( b

:: deftheorem Def13 defines zeros PRVECT_1:def 14 :

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b_{2} being Element of product (carr g) holds

( b_{2} = zeros g iff for i being Element of dom (carr g) holds b_{2} . i = 0. (g . i) );

for g being non empty non-empty-addLoopStr-yielding FinSequence

for b

( b

definition

let G be non empty non-empty-addLoopStr-yielding FinSequence;

addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is non empty strict addLoopStr ;

end;
func product G -> non empty strict addLoopStr equals :: PRVECT_1:def 15

addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);

coherence addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);

addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is non empty strict addLoopStr ;

:: deftheorem defines product PRVECT_1:def 15 :

for G being non empty non-empty-addLoopStr-yielding FinSequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);

for G being non empty non-empty-addLoopStr-yielding FinSequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);

registration

let G be Group-Sequence;

coherence

( product G is add-associative & product G is right_zeroed & product G is right_complementable & not product G is empty & product G is Abelian )

end;
coherence

( product G is add-associative & product G is right_zeroed & product G is right_complementable & not product G is empty & product G is Abelian )

proof end;