:: PRVECT_1 semantic presentation

begin

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

deffunc H2( addLoopStr ) ->  Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;

deffunc H3( non empty addLoopStr ) ->  Element of bool [: the carrier of $1, the carrier of $1:] = comp $1;

deffunc H4( addLoopStr ) ->  Element of the carrier of $1 = 0. $1;

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
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: 0. G is_a_unity_wrt the addF of G
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._((0._G),x)_=_x_&_the_addF_of_G_._(x,(0._G))_=_x_)
let x be Element of G; ::_thesis: ( the addF of G . ((0. G),x) = x & the addF of G . (x,(0. G)) = x )
thus  the addF of G . ((0. G),x) = (0. G) + x
.= x by RLVECT_1:4 ; ::_thesis: the addF of G . (x,(0. G)) = x
thus  the addF of G . (x,(0. G)) = x + (0. G)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
hence  0. G is_a_unity_wrt the addF of G by BINOP_1:3; ::_thesis: verum
end;

theorem Th2: :: PRVECT_1:2
for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G
proof
let G be AbGroup; ::_thesis: comp G is_an_inverseOp_wrt the addF of G
A1: 0. G is_a_unity_wrt the addF of G by Th1;
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._(x,((comp_G)_._x))_=_the_unity_wrt_the_addF_of_G_&_the_addF_of_G_._(((comp_G)_._x),x)_=_the_unity_wrt_the_addF_of_G_)
let x be Element of G; ::_thesis: ( the addF of G . (x,((comp G) . x)) = the_unity_wrt the addF of G & the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G )
thus  the addF of G . (x,((comp G) . x)) = x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G
thus  the addF of G . (((comp G) . x),x) = ((comp G) . x) + x
.= x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: verum
end;
hence  comp G is_an_inverseOp_wrt the addF of G by FINSEQOP:def_1; ::_thesis: verum
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
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: comp G is_an_inverseOp_wrt the addF of G
A1: 0. G is_a_unity_wrt the addF of G by Th1;
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._(x,((comp_G)_._x))_=_the_unity_wrt_the_addF_of_G_&_the_addF_of_G_._(((comp_G)_._x),x)_=_the_unity_wrt_the_addF_of_G_)
let x be Element of G; ::_thesis: ( the addF of G . (x,((comp G) . x)) = the_unity_wrt the addF of G & the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G )
thus  the addF of G . (x,((comp G) . x)) = x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G
thus  the addF of G . (((comp G) . x),x) = ((comp G) . x) + x
.= x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: verum
end;
hence  comp G is_an_inverseOp_wrt the addF of G by FINSEQOP:def_1; ::_thesis: verum
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
proof
let GS be non empty addLoopStr ; ::_thesis: ( 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 implies GS is AbGroup )
assume that
A1: ( the addF of GS is commutative & the addF of GS is associative ) and
A2: 0. GS is_a_unity_wrt the addF of GS and
A3: comp GS is_an_inverseOp_wrt the addF of GS ; ::_thesis: GS is AbGroup
A4: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider b = (comp GS) . x as Element of GS ;
take  b ; :: according to ALGSTR_0:def_11 ::_thesis: x + b = 0. GS
thus x + b = the_unity_wrt the addF of GS by A3, FINSEQOP:def_1
.= 0. GS by A2, BINOP_1:def_8 ; ::_thesis: verum
end;
 for x, y, z being Element of GS holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. GS) = x ) by A1, A2, BINOP_1:3, BINOP_1:def_2, BINOP_1:def_3;
hence  GS is AbGroup by A4, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
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 )
proof
let GS be non empty addLoopStr ; ::_thesis: ( the addF of GS is commutative & the addF of GS is associative implies ( GS is Abelian & GS is add-associative ) )
assume that
A1: the addF of GS is commutative and
A2: the addF of GS is associative ; ::_thesis: ( GS is Abelian & GS is add-associative )
thus  GS is Abelian ::_thesis: GS is add-associative
proof
let x, y be Element of GS; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
thus  x + y = y + x by A1, BINOP_1:def_2; ::_thesis: verum
end;
let x, y, z be Element of GS; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
thus  (x + y) + z = x + (y + z) by A2, BINOP_1:def_3; ::_thesis: verum
end;

Lm3:  for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
proof
let GS be non empty addLoopStr ; ::_thesis: ( 0. GS is_a_unity_wrt the addF of GS implies GS is right_zeroed )
assume A1: 0. GS is_a_unity_wrt the addF of GS ; ::_thesis: GS is right_zeroed
let x be Element of GS; :: according to RLVECT_1:def_4 ::_thesis: x + (0. GS) = x
thus  x + (0. GS) = x by A1, BINOP_1:3; ::_thesis: verum
end;

 Lm4:  for F being Field holds the multF of F is associative
proof
let F be Field; ::_thesis: the multF of F is associative
let x, y, z be Element of F; :: according to BINOP_1:def_3 ::_thesis: the multF of F . (x,( the multF of F . (y,z))) = the multF of F . (( the multF of F . (x,y)),z)
thus  the multF of F . (x,( the multF of F . (y,z))) = x * (y * z)
.= (x * y) * z by GROUP_1:def_3
.= the multF of F . (( the multF of F . (x,y)),z) ; ::_thesis: verum
end;

theorem :: PRVECT_1:4
for F being Field holds 0. F is_a_unity_wrt the addF of F
proof
let F be Field; ::_thesis: 0. F is_a_unity_wrt the addF of F
now__::_thesis:_for_x_being_Element_of_F_holds_
(_the_addF_of_F_._((0._F),x)_=_x_&_the_addF_of_F_._(x,(0._F))_=_x_)
let x be Element of F; ::_thesis: ( the addF of F . ((0. F),x) = x & the addF of F . (x,(0. F)) = x )
thus  the addF of F . ((0. F),x) = x + (0. F) by RLVECT_1:2
.= x by RLVECT_1:4 ; ::_thesis: the addF of F . (x,(0. F)) = x
thus  the addF of F . (x,(0. F)) = x + (0. F)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
hence  0. F is_a_unity_wrt the addF of F by BINOP_1:3; ::_thesis: verum
end;

theorem Th5: :: PRVECT_1:5
for F being Field holds 1_ F is_a_unity_wrt the multF of F
proof
let F be Field; ::_thesis: 1_ F is_a_unity_wrt the multF of F
now__::_thesis:_for_x_being_Element_of_F_holds_
(_the_multF_of_F_._((1__F),x)_=_x_&_the_multF_of_F_._(x,(1__F))_=_x_)
let x be Element of F; ::_thesis: ( the multF of F . ((1_ F),x) = x & the multF of F . (x,(1_ F)) = x )
thus  the multF of F . ((1_ F),x) = (1_ F) * x
.= x by VECTSP_1:def_8 ; ::_thesis: the multF of F . (x,(1_ F)) = x
thus  the multF of F . (x,(1_ F)) = x * (1_ F)
.= x by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence  1_ F is_a_unity_wrt the multF of F by BINOP_1:3; ::_thesis: verum
end;

Lm5:  for F being Field holds the multF of F is_distributive_wrt the addF of F
proof
let F be Field; ::_thesis: the multF of F is_distributive_wrt the addF of F
now__::_thesis:_for_x,_y,_z_being_Element_of_F_holds_
(_the_multF_of_F_._(x,(_the_addF_of_F_._(y,z)))_=_the_addF_of_F_._((_the_multF_of_F_._(x,y)),(_the_multF_of_F_._(x,z)))_&_the_multF_of_F_._((_the_addF_of_F_._(x,y)),z)_=_the_addF_of_F_._((_the_multF_of_F_._(x,z)),(_the_multF_of_F_._(y,z)))_)
let x, y, z be Element of F; ::_thesis: ( the multF of F . (x,( the addF of F . (y,z))) = the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) & the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) )
thus  the multF of F . (x,( the addF of F . (y,z))) = x * (y + z)
.= (x * y) + (x * z) by VECTSP_1:def_7
.= the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) ; ::_thesis: the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z)))
thus  the multF of F . (( the addF of F . (x,y)),z) = (x + y) * z
.= (x * z) + (y * z) by VECTSP_1:def_7
.= the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) ; ::_thesis: verum
end;
hence  the multF of F is_distributive_wrt the addF of F by BINOP_1:11; ::_thesis: verum
end;

begin


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 funcF .: (x,y) ->  Element of n -tuples_on D;
coherence
 F .: (x,y) is Element of n -tuples_on D by FINSEQ_2:120;
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
defpred S1[ set , set , set ] means  ex x9, y9 being Element of n -tuples_on D st
( $1 = x9 & $2 = y9 & $3 = F .: (x9,y9) );
A1: for x, y being Element of n -tuples_on D ex z being Element of n -tuples_on D st S1[x,y,z]
proof
let x, y be Element of n -tuples_on D; ::_thesis: ex z being Element of n -tuples_on D st S1[x,y,z]
reconsider x9 = x, y9 = y as Element of n -tuples_on D ;
reconsider z = F .: (x9,y9) as Element of n -tuples_on D ;
take  z ; ::_thesis: S1[x,y,z]
take  x9 ; ::_thesis: ex y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & z = F .: (x9,y9) )
take  y9 ; ::_thesis: ( x = x9 & y = y9 & z = F .: (x9,y9) )
thus  ( x = x9 & y = y9 & z = F .: (x9,y9) ) ; ::_thesis: verum
end;
consider G being BinOp of (n -tuples_on D) such that
A2: for x, y being Element of n -tuples_on D holds S1[x,y,G . (x,y)] from BINOP_1:sch_3(A1);
take  G ; ::_thesis: for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y)
let p1, p2 be Element of n -tuples_on D; ::_thesis: G . (p1,p2) = F .: (p1,p2)
reconsider x = p1, y = p2 as Element of n -tuples_on D ;
 ex x9, y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & G . (x,y) = F .: (x9,y9) ) by A2;
hence  G . (p1,p2) = F .: (p1,p2) ; ::_thesis: verum
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
let G, H be BinOp of (n -tuples_on D); ::_thesis: ( ( for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds H . (x,y) = F .: (x,y) ) implies G = H )
assume that
A3: for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y) and
A4: for x, y being Element of n -tuples_on D holds H . (x,y) = F .: (x,y) ; ::_thesis: G = H
now__::_thesis:_for_x,_y_being_Element_of_n_-tuples_on_D_holds_G_._(x,y)_=_H_._(x,y)
let x, y be Element of n -tuples_on D; ::_thesis: G . (x,y) = H . (x,y)
 G . (x,y) = F .: (x,y) by A3;
hence  G . (x,y) = H . (x,y) by A4; ::_thesis: verum
end;
hence  G = H by BINOP_1:2; ::_thesis: verum
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
defpred S1[ set , set ] means  ex x9 being Element of n -tuples_on D st
( x9 = $1 & $2 = F * x9 );
A1: for x being Element of n -tuples_on D ex y being Element of n -tuples_on D st S1[x,y]
proof
let x be Element of n -tuples_on D; ::_thesis: ex y being Element of n -tuples_on D st S1[x,y]
reconsider x9 = x as Element of n -tuples_on D ;
reconsider y = F * x9 as Element of n -tuples_on D by FINSEQ_2:113;
take  y ; ::_thesis: S1[x,y]
take  x9 ; ::_thesis: ( x9 = x & y = F * x9 )
thus  ( x9 = x & y = F * x9 ) ; ::_thesis: verum
end;
consider G being UnOp of (n -tuples_on D) such that
A2: for x being Element of n -tuples_on D holds S1[x,G . x] from FUNCT_2:sch_3(A1);
take  G ; ::_thesis: for x being Element of n -tuples_on D holds G . x = F * x
let p1 be Element of n -tuples_on D; ::_thesis: G . p1 = F * p1
reconsider x = p1 as Element of n -tuples_on D ;
 ex x9 being Element of n -tuples_on D st
( x9 = x & G . x = F * x9 ) by A2;
hence  G . p1 = F * p1 ; ::_thesis: verum
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
let G, H be UnOp of (n -tuples_on D); ::_thesis: ( ( for x being Element of n -tuples_on D holds G . x = F * x ) & ( for x being Element of n -tuples_on D holds H . x = F * x ) implies G = H )
assume that
A3: for x being Element of n -tuples_on D holds G . x = F * x and
A4: for x being Element of n -tuples_on D holds H . x = F * x ; ::_thesis: G = H
now__::_thesis:_for_x_being_Element_of_n_-tuples_on_D_holds_G_._x_=_H_._x
let x be Element of n -tuples_on D; ::_thesis: G . x = H . x
 G . x = F * x by A3;
hence  G . x = H . x by A4; ::_thesis: verum
end;
hence  G = H by FUNCT_2:63; ::_thesis: verum
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 );

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
proof
let n be Nat; ::_thesis: for D being non empty set
for B being BinOp of D st B is commutative holds
product (B,n) is commutative
let D be non empty set ; ::_thesis: for B being BinOp of D st B is commutative holds
product (B,n) is commutative
let B be BinOp of D; ::_thesis: ( B is commutative implies product (B,n) is commutative )
assume A1: B is commutative ; ::_thesis: product (B,n) is commutative
now__::_thesis:_for_x,_y_being_Element_of_n_-tuples_on_D_holds_(product_(B,n))_._(x,y)_=_(product_(B,n))_._(y,x)
let x, y be Element of n -tuples_on D; ::_thesis: (product (B,n)) . (x,y) = (product (B,n)) . (y,x)
thus (product (B,n)) . (x,y) = B .: (x,y) by Def1
.= B .: (y,x) by A1, FINSEQOP:33
.= (product (B,n)) . (y,x) by Def1 ; ::_thesis: verum
end;
hence  product (B,n) is commutative by BINOP_1:def_2; ::_thesis: verum
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
proof
let n be Nat; ::_thesis: for D being non empty set
for B being BinOp of D st B is associative holds
product (B,n) is associative
let D be non empty set ; ::_thesis: for B being BinOp of D st B is associative holds
product (B,n) is associative
let B be BinOp of D; ::_thesis: ( B is associative implies product (B,n) is associative )
assume A1: B is associative ; ::_thesis: product (B,n) is associative
now__::_thesis:_for_x,_y,_z_being_Element_of_n_-tuples_on_D_holds_(product_(B,n))_._(((product_(B,n))_._(x,y)),z)_=_(product_(B,n))_._(x,((product_(B,n))_._(y,z)))
let x, y, z be Element of n -tuples_on D; ::_thesis: (product (B,n)) . (((product (B,n)) . (x,y)),z) = (product (B,n)) . (x,((product (B,n)) . (y,z)))
thus (product (B,n)) . (((product (B,n)) . (x,y)),z) = (product (B,n)) . ((B .: (x,y)),z) by Def1
.= B .: ((B .: (x,y)),z) by Def1
.= B .: (x,(B .: (y,z))) by A1, FINSEQOP:28
.= (product (B,n)) . (x,(B .: (y,z))) by Def1
.= (product (B,n)) . (x,((product (B,n)) . (y,z))) by Def1 ; ::_thesis: verum
end;
hence  product (B,n) is associative by BINOP_1:def_3; ::_thesis: verum
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)
proof
let n be Nat; ::_thesis: 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)
let D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
let B be BinOp of D; ::_thesis: ( d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product (B,n) )
assume  d is_a_unity_wrt B ; ::_thesis: n |-> d is_a_unity_wrt product (B,n)
then A1: ( B is having_a_unity & d = the_unity_wrt B ) by BINOP_1:def_8, SETWISEO:def_2;
now__::_thesis:_for_b_being_Element_of_n_-tuples_on_D_holds_
(_(product_(B,n))_._((n_|->_d),b)_=_b_&_(product_(B,n))_._(b,(n_|->_d))_=_b_)
let b be Element of n -tuples_on D; ::_thesis: ( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )
reconsider b9 = b as Element of n -tuples_on D ;
thus (product (B,n)) . ((n |-> d),b) = B .: ((n |-> d),b9) by Def1
.= b by A1, FINSEQOP:56 ; ::_thesis: (product (B,n)) . (b,(n |-> d)) = b
thus (product (B,n)) . (b,(n |-> d)) = B .: (b9,(n |-> d)) by Def1
.= b by A1, FINSEQOP:56 ; ::_thesis: verum
end;
hence  n |-> d is_a_unity_wrt product (B,n) by BINOP_1:3; ::_thesis: verum
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)
proof
let n be Nat; ::_thesis: 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)
let D be non empty set ; ::_thesis: 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)
let B be BinOp of D; ::_thesis: 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)
let C be UnOp of D; ::_thesis: ( B is having_a_unity & B is associative & C is_an_inverseOp_wrt B implies product (C,n) is_an_inverseOp_wrt product (B,n) )
assume that
A1: B is having_a_unity and
A2: B is associative and
A3: C is_an_inverseOp_wrt B ; ::_thesis: product (C,n) is_an_inverseOp_wrt product (B,n)
A4: B is having_an_inverseOp by A3, FINSEQOP:def_2;
then A5: C = the_inverseOp_wrt B by A1, A2, A3, FINSEQOP:def_3;
A6: now__::_thesis:_for_f_being_Element_of_n_-tuples_on_D_holds_
(_(product_(B,n))_._(f,((product_(C,n))_._f))_=_n_|->_(the_unity_wrt_B)_&_(product_(B,n))_._(((product_(C,n))_._f),f)_=_n_|->_(the_unity_wrt_B)_)
let f be Element of n -tuples_on D; ::_thesis: ( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> (the_unity_wrt B) & (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B) )
reconsider f9 = f as Element of n -tuples_on D ;
reconsider cf = C * f9 as Element of n -tuples_on D by FINSEQ_2:113;
thus (product (B,n)) . (f,((product (C,n)) . f)) = (product (B,n)) . (f9,(C * f9)) by Def2
.= B .: (f9,cf) by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:73 ; ::_thesis: (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B)
thus (product (B,n)) . (((product (C,n)) . f),f) = (product (B,n)) . ((C * f9),f9) by Def2
.= B .: (cf,f9) by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:73 ; ::_thesis: verum
end;
 ex d being Element of D st d is_a_unity_wrt B by A1, SETWISEO:def_2;
then  the_unity_wrt B is_a_unity_wrt B by BINOP_1:def_8;
then  n |-> (the_unity_wrt B) is_a_unity_wrt product (B,n) by Th8;
then  n |-> (the_unity_wrt B) = the_unity_wrt (product (B,n)) by BINOP_1:def_8;
hence  product (C,n) is_an_inverseOp_wrt product (B,n) by A6, FINSEQOP:def_1; ::_thesis: verum
end;

begin

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 ) ;
funcn -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)) #) is strict AbGroup
proof
set G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);
reconsider G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) as non empty addLoopStr ;
 ( the addF of F is commutative & the addF of F is associative ) by A1, FVSUM_1:1, FVSUM_1:2;
then A2: ( product ( the addF of F,n) is commutative & product ( the addF of F,n) is associative ) by Th6, Th7;
A3: 0. F is_a_unity_wrt the addF of F by A1, Th1;
A4: G is right_complementable
proof
set B = the addF of F;
set C = comp F;
let x be Element of G; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider y = (product ((comp F),n)) . x as Element of G by FUNCT_2:5;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. G
 ( the addF of F is associative & the addF of F is having_a_unity ) by A1, A3, FVSUM_1:2, SETWISEO:def_2;
then  product ((comp F),n) is_an_inverseOp_wrt product ( the addF of F,n) by A1, Lm1, Th9;
then A5: x + y = the_unity_wrt (product ( the addF of F,n)) by FINSEQOP:def_1;
 0. G is_a_unity_wrt the addF of G by A1, Th1, Th8;
hence  x + y = 0. G by A5, BINOP_1:def_8; ::_thesis: verum
end;
 ( 0. G = n |-> (0. F) & n |-> (0. F) is_a_unity_wrt product ( the addF of F,n) ) by A1, Th1, Th8;
hence  addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup by A2, A4, Lm2, Lm3; ::_thesis: verum
end;
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)) #);

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


definition
let F be Field;
let n be Nat;
funcn -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
 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 multF of F [;] (x,v)
proof
defpred S1[ set , set ] means  ex x1 being Element of F ex v being Element of n -tuples_on the carrier of F st
( $1 = [x1,v] & $2 = the multF of F [;] (x1,v) );
A1: for x being set st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [: the carrier of F,(n -tuples_on the carrier of F):] implies ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] ) )
assume  x in [: the carrier of F,(n -tuples_on the carrier of F):] ; ::_thesis: ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] )
then consider x1, v being set  such that
A2: x1 in the carrier of F and
A3: v in n -tuples_on the carrier of F and
A4: [x1,v] = x by ZFMISC_1:84;
reconsider v = v as Element of n -tuples_on the carrier of F by A3;
reconsider x1 = x1 as Element of F by A2;
take y = the multF of F [;] (x1,v); ::_thesis: ( y in n -tuples_on the carrier of F & S1[x,y] )
 y is Element of n -tuples_on the carrier of F by FINSEQ_2:121;
hence  y in n -tuples_on the carrier of F ; ::_thesis: S1[x,y]
take  x1 ; ::_thesis: ex v being Element of n -tuples_on the carrier of F st
( x = [x1,v] & y = the multF of F [;] (x1,v) )
take  v ; ::_thesis: ( x = [x1,v] & y = the multF of F [;] (x1,v) )
thus  ( x = [x1,v] & y = the multF of F [;] (x1,v) ) by A4; ::_thesis: verum
end;
consider f being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) such that
A5: for x being set st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
take  f ; ::_thesis: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)
let x be Element of F; ::_thesis: for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)
let v be Element of n -tuples_on the carrier of F; ::_thesis: f . (x,v) = the multF of F [;] (x,v)
 [x,v] in [: the carrier of F,(n -tuples_on the carrier of F):] by ZFMISC_1:87;
then consider x1 being Element of F, v1 being Element of n -tuples_on the carrier of F such that
A6: [x,v] = [x1,v1] and
A7: f . [x,v] = the multF of F [;] (x1,v1) by A5;
 x1 = x by A6, XTUPLE_0:1;
hence  f . (x,v) = the multF of F [;] (x,v) by A6, A7, XTUPLE_0:1; ::_thesis: verum
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 multF 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 multF of F [;] (x,v) ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F); ::_thesis: ( ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (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 g . (x,v) = the multF of F [;] (x,v) ) implies f = g )
assume that
A8: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v) and
A9: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds g . (x,v) = the multF of F [;] (x,v) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_F
for_v_being_Element_of_n_-tuples_on_the_carrier_of_F_holds_f_._(x,v)_=_g_._(x,v)
let x be Element of F; ::_thesis: for v being Element of n -tuples_on the carrier of F holds f . (x,v) = g . (x,v)
let v be Element of n -tuples_on the carrier of F; ::_thesis: f . (x,v) = g . (x,v)
 f . (x,v) = the multF of F [;] (x,v) by A8;
hence  f . (x,v) = g . (x,v) by A9; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
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 multF of F [;] (x,v) );

definition
let F be Field;
let n be Nat;
funcn -VectSp_over F ->  strict VectSpStr 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
 ex b1 being strict VectSpStr over F st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F )
proof
 n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) by Def3;
then reconsider d = n -Mult_over F as Function of [: the carrier of F, the carrier of (n -Group_over F):], the carrier of (n -Group_over F) ;
set G = n -Group_over F;
take  VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) ; ::_thesis: ( addLoopStr(# the carrier of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the addF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the ZeroF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) = n -Mult_over F )
thus  ( addLoopStr(# the carrier of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the addF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the ZeroF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) = n -Mult_over F ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict VectSpStr over F st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF 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 over F holds
( b3 = n -VectSp_over F iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = n -Group_over F & the lmult of b3 = n -Mult_over F ) );

registration
let F be Field;
let n be Nat;
clustern -VectSp_over F ->  non empty strict ;
coherence
 not n -VectSp_over F is empty
proof
 addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F by Def5;
hence  not the carrier of (n -VectSp_over F) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;


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)))
proof
let n be Nat; ::_thesis: 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)))
let D be non empty set ; ::_thesis: 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)))
let H, G be BinOp of D; ::_thesis: 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)))
let d be Element of D; ::_thesis: 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)))
let t1, t2 be Element of n -tuples_on D; ::_thesis: ( H is_distributive_wrt G implies H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) )
A1: H [;] (d,(G .: (t1,t2))) = H [;] (d,(G * <:t1,t2:>)) by FUNCOP_1:def_3
.= H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> by FUNCOP_1:def_5 ;
 ( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H ) by RELAT_1:26;
then  ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] & [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] c= [:(rng H),(rng H):] ) by FUNCT_3:51, ZFMISC_1:96;
then A2: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):] by XBOOLE_1:1;
 rng H c= D by RELAT_1:def_19;
then  [:(rng H),(rng H):] c= [:D,D:] by ZFMISC_1:96;
then  rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:] by A2, XBOOLE_1:1;
then A3: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G by FUNCT_2:def_1;
A4: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def_4;
then A5: [:(rng t1),(rng t2):] c= [:D,D:] by ZFMISC_1:96;
 rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:51;
then  rng <:t1,t2:> c= [:D,D:] by A5, XBOOLE_1:1;
then A6: rng <:t1,t2:> c= dom G by FUNCT_2:def_1;
A7: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then  dom <:t1,t2:> = Seg n by A4, FUNCT_3:50;
then A8: dom (G * <:t1,t2:>) = Seg n by A6, RELAT_1:27;
then  dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:13;
then A9: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A8, FUNCT_3:50;
 rng t2 c= D by FINSEQ_1:def_4;
then  ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A10: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;
 rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;
then  [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A11: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A10, XBOOLE_1:1;
A12: dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 rng t1 c= D by FINSEQ_1:def_4;
then  ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A13: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;
 rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;
then  [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A14: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A13, XBOOLE_1:1;
A15: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 {d} c= D by ZFMISC_1:31;
then A16: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
 ( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:13, ZFMISC_1:31;
then A17: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;
A18: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 dom H = [:D,D:] by FUNCT_2:def_1;
then A19: dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A11, A16, RELAT_1:27, XBOOLE_1:1
.= Seg n by A7, A18, FUNCT_3:50 ;
 {d} c= D by ZFMISC_1:31;
then A20: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;
A21: G .: ((H [;] (d,t1)),(H [;] (d,t2))) = G .: ((H * <:((dom t1) --> d),t1:>),(H [;] (d,t2))) by FUNCOP_1:def_5
.= G .: ((H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>)) by FUNCOP_1:def_5
.= G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> by FUNCOP_1:def_3 ;
 dom H = [:D,D:] by FUNCT_2:def_1;
then  dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A14, A20, RELAT_1:27, XBOOLE_1:1
.= Seg n by A15, A12, FUNCT_3:50 ;
then  dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A19, FUNCT_3:50;
then A22: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A3, RELAT_1:27;
 rng (G * <:t1,t2:>) c= D by RELAT_1:def_19;
then  ( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] & [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] ) by A17, FUNCT_3:51, ZFMISC_1:96;
then  rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] by XBOOLE_1:1;
then A23: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H by FUNCT_2:def_1;
then A24: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A9, RELAT_1:27;
assume A25: H is_distributive_wrt G ; ::_thesis: H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
 for x being set st x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) holds
(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
proof
 rng t1 c= D by FINSEQ_1:def_4;
then  ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A26: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;
 rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;
then  [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A27: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A26, XBOOLE_1:1;
A28: ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def_4;
 {d} c= D by ZFMISC_1:31;
then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A30: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 {d} c= D by ZFMISC_1:31;
then A31: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A32: dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 rng t2 c= D by FINSEQ_1:def_4;
then  ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A33: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;
 rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;
then  [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A34: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A33, XBOOLE_1:1;
A35: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
let x be set ; ::_thesis: ( x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) implies (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x )
A36: dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> = (dom ((dom (G .: (t1,t2))) --> d)) /\ (dom (G .: (t1,t2))) by FUNCT_3:def_7;
assume A37: x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) ; ::_thesis: (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
then  x in dom (H * <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):>) by A1, FUNCOP_1:def_5;
then  x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> by FUNCT_1:11;
then A38: x in dom (G .: (t1,t2)) by A36, XBOOLE_0:def_4;
dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then A39: t1 . x in rng t1 by A24, A37, FUNCT_1:def_3;
A40: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 dom H = [:D,D:] by FUNCT_2:def_1;
then  dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A27, A31, RELAT_1:27, XBOOLE_1:1
.= Seg n by A35, A32, FUNCT_3:50 ;
then A41: x in dom (H [;] (d,t1)) by A24, A37, FUNCOP_1:def_5;
dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then A42: t2 . x in rng t2 by A24, A37, FUNCT_1:def_3;
 dom H = [:D,D:] by FUNCT_2:def_1;
then  dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A34, A29, RELAT_1:27, XBOOLE_1:1
.= Seg n by A30, A40, FUNCT_3:50 ;
then A43: x in dom (H [;] (d,t2)) by A24, A37, FUNCOP_1:def_5;
(H [;] (d,(G .: (t1,t2)))) . x = H . (d,((G .: (t1,t2)) . x)) by A1, A37, FUNCOP_1:32
.= H . (d,(G . ((t1 . x),(t2 . x)))) by A38, FUNCOP_1:22
.= G . ((H . (d,(t1 . x))),(H . (d,(t2 . x)))) by A25, A39, A28, A42, BINOP_1:11
.= G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x)))) by A41, FUNCOP_1:32
.= G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x)) by A43, FUNCOP_1:32
.= (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x by A21, A24, A22, A37, FUNCOP_1:22 ;
hence  (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x ; ::_thesis: verum
end;
hence  H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) by A1, A21, A9, A23, A22, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
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 funcF [;] (x,v) ->  Element of n -tuples_on D;
coherence
 F [;] (x,v) is Element of n -tuples_on D by FINSEQ_2:121;
end;

registration
let F be Field;
let n be Nat;
clustern -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
A1: ( addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F & n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) ) by Def3, Def5;
 1_ F is_a_unity_wrt the multF of F by Th5;
then A2: ( the multF of F is having_a_unity & the_unity_wrt the multF of F = 1_ F ) by BINOP_1:def_8, SETWISEO:def_2;
A3: n -VectSp_over F is vector-distributive
proof
let x be Element of F; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of (n -VectSp_over F) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of (n -VectSp_over F); ::_thesis: x * (v + w) = (x * v) + (x * w)
reconsider v9 = v, w9 = w as Element of n -tuples_on the carrier of F by A1;
thus x * (v + w) = (n -Mult_over F) . (x,((product ( the addF of F,n)) . (v,w))) by A1, Def5
.= (n -Mult_over F) . (x,( the addF of F .: (v9,w9))) by Def1
.= the multF of F [;] (x,( the addF of F .: (v9,w9))) by Def4
.= the addF of F .: (( the multF of F [;] (x,v9)),( the multF of F [;] (x,w9))) by Lm5, Th10
.= (product ( the addF of F,n)) . (( the multF of F [;] (x,v9)),( the multF of F [;] (x,w9))) by Def1
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),( the multF of F [;] (x,w9))) by Def4
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (x,w9))) by Def4
.= (product ( the addF of F,n)) . (( the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (x,w9))) by Def5
.= (x * v) + (x * w) by A1, Def5 ; ::_thesis: verum
end;
A4: n -VectSp_over F is scalar-distributive
proof
let x, y be Element of F; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of (n -VectSp_over F) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of (n -VectSp_over F); ::_thesis: (x + y) * v = (x * v) + (y * v)
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (x + y) * v = (n -Mult_over F) . ((x + y),v9) by Def5
.= the multF of F [;] (( the addF of F . (x,y)),v9) by Def4
.= the addF of F .: (( the multF of F [;] (x,v9)),( the multF of F [;] (y,v9))) by Lm5, FINSEQOP:46
.= (product ( the addF of F,n)) . (( the multF of F [;] (x,v9)),( the multF of F [;] (y,v9))) by Def1
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),( the multF of F [;] (y,v9))) by Def4
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (y,v9))) by Def4
.= (product ( the addF of F,n)) . (( the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (y,v9))) by Def5
.= (x * v) + (y * v) by A1, Def5 ; ::_thesis: verum
end;
A5: n -VectSp_over F is scalar-associative
proof
let x, y be Element of F; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of (n -VectSp_over F) holds (x * y) * b1 = x * (y * b1)
let v be Element of (n -VectSp_over F); ::_thesis: (x * y) * v = x * (y * v)
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (x * y) * v = (n -Mult_over F) . ((x * y),v9) by Def5
.= the multF of F [;] ((x * y),v9) by Def4
.= the multF of F [;] (x,( the multF of F [;] (y,v9))) by Lm4, FINSEQOP:31
.= (n -Mult_over F) . (x,( the multF of F [;] (y,v9))) by Def4
.= (n -Mult_over F) . (x,((n -Mult_over F) . (y,v9))) by Def4
.= (n -Mult_over F) . (x,( the lmult of (n -VectSp_over F) . (y,v))) by Def5
.= x * (y * v) by Def5 ; ::_thesis: verum
end;
 n -VectSp_over F is scalar-unital
proof
let v be Element of (n -VectSp_over F); :: according to VECTSP_1:def_17 ::_thesis: (1. F) * v = v
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (1. F) * v = (n -Mult_over F) . ((1. F),v9) by Def5
.= the multF of F [;] ((1. F),v9) by Def4
.= v by A2, FINSEQOP:57 ; ::_thesis: verum
end;
hence  ( 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 ) by A3, A4, A5; ::_thesis: verum
end;
end;

begin


definition
mode Domain-Sequence is non-empty non empty FinSequence;
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
consider p being FinSequence such that
A1: ( len p = len F1() & ( for i being Nat st i in dom p holds
p . i = F2(i) ) ) from FINSEQ_1:sch_2();
 dom p = dom F1() by A1, FINSEQ_3:29;
then reconsider p9 = p as non empty FinSequence ;
take  p9 ; ::_thesis: ( len p9 = len F1() & ( for i being Element of dom F1() holds p9 . i = F2(i) ) )
thus  len p9 = len F1() by A1; ::_thesis: for i being Element of dom F1() holds p9 . i = F2(i)
let i be Element of dom F1(); ::_thesis: p9 . i = F2(i)
A2: dom F1() = Seg (len F1()) by FINSEQ_1:def_3;
 dom p = Seg (len F1()) by A1, FINSEQ_1:def_3;
hence  p9 . i = F2(i) by A1, A2; ::_thesis: verum
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 funcf . i ->  Element of a . i;
coherence
 f . i is Element of a . i by CARD_3:9;
end;

begin


definition
let a be non-empty non empty Function;
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
 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
deffunc H5( set ) ->  Element of bool [:[:(a . $1),(a . $1):],(a . $1):] = pr1 ((a . $1),(a . $1));
consider f being Function such that
A1: ( dom f = dom a & ( for x being set st x in dom a holds
f . x = H5(x) ) ) from FUNCT_1:sch_3();
take  f ; ::_thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is BinOp of (a . i) ) )
thus  dom f = dom a by A1; ::_thesis: for i being Element of dom a holds f . i is BinOp of (a . i)
let i be Element of dom a; ::_thesis: f . i is BinOp of (a . i)
 f . i = pr1 ((a . i),(a . i)) by A1;
hence  f . i is BinOp of (a . i) ; ::_thesis: verum
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
 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
deffunc H5( set ) ->  Element of bool [:(a . $1),(a . $1):] = id (a . $1);
consider f being Function such that
A2: ( dom f = dom a & ( for x being set st x in dom a holds
f . x = H5(x) ) ) from FUNCT_1:sch_3();
take  f ; ::_thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is UnOp of (a . i) ) )
thus  dom f = dom a by A2; ::_thesis: for i being Element of dom a holds f . i is UnOp of (a . i)
let i be Element of dom a; ::_thesis: f . i is UnOp of (a . i)
 f . i = id (a . i) by A2;
hence  f . i is UnOp of (a . i) ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines BinOps PRVECT_1:def_6_:_
 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 Def7 defines UnOps PRVECT_1:def_7_:_
 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 for BinOps of a;
coherence
 for b1 being BinOps of a holds b1 is FinSequence-like
proof
let f be BinOps of a; ::_thesis: f is FinSequence-like
 ( dom a = dom f & dom a = Seg (len a) ) by Def6, FINSEQ_1:def_3;
hence  f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
cluster  ->  FinSequence-like for UnOps of a;
coherence
 for b1 being UnOps of a holds b1 is FinSequence-like
proof
let f be UnOps of a; ::_thesis: f is FinSequence-like
 ( dom a = dom f & dom a = Seg (len a) ) by Def7, FINSEQ_1:def_3;
hence  f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
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) ) ) )
proof
let a be Domain-Sequence; ::_thesis: 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) ) ) )
let p be FinSequence; ::_thesis: ( 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) ) ) )
 ( dom p = dom a iff len p = len a ) by FINSEQ_3:29;
hence  ( 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) ) ) ) by Def6; ::_thesis: verum
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) ) ) )
proof
let a be Domain-Sequence; ::_thesis: 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) ) ) )
let p be FinSequence; ::_thesis: ( 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) ) ) )
 ( dom p = dom a iff len p = len a ) by FINSEQ_3:29;
hence  ( 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) ) ) ) by Def7; ::_thesis: verum
end;

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

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

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
proof
let a be Domain-Sequence; ::_thesis: 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
let d, d9 be UnOp of (product a); ::_thesis: ( ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) implies d = d9 )
assume A1: for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ; ::_thesis: d = d9
now__::_thesis:_for_f_being_Element_of_product_a_holds_d_._f_=_d9_._f
let f be Element of product a; ::_thesis: d . f = d9 . f
A2: ( dom (d . f) = dom a & dom (d9 . f) = dom a ) by CARD_3:9;
 for x being set st x in dom a holds
(d . f) . x = (d9 . f) . x by A1;
hence  d . f = d9 . f by A2, FUNCT_1:2; ::_thesis: verum
end;
hence  d = d9 by FUNCT_2:63; ::_thesis: verum
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 )
proof
let a be Domain-Sequence; ::_thesis: for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
let u be UnOps of a; ::_thesis: ( doms u = a & product (rngs u) c= product a )
A1: dom (doms u) = u " (SubFuncs (rng u)) by FUNCT_6:def_2;
A2: ( dom a = Seg (len a) & dom u = Seg (len u) ) by FINSEQ_1:def_3;
A3: len u = len a by Th12;
A4: dom u c= u " (SubFuncs (rng u))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom u or x in u " (SubFuncs (rng u)) )
assume  x in dom u ; ::_thesis: x in u " (SubFuncs (rng u))
then reconsider x = x as Element of dom a by A2, Th12;
 u . x is UnOp of (a . x) ;
hence  x in u " (SubFuncs (rng u)) by A2, A3, FUNCT_6:19; ::_thesis: verum
end;
 u " (SubFuncs (rng u)) c= dom u by RELAT_1:132;
then A5: dom (doms u) = dom u by A1, A4, XBOOLE_0:def_10;
A6: now__::_thesis:_for_x_being_set_st_x_in_dom_u_holds_
(rngs_u)_._x_c=_a_._x
let x be set ; ::_thesis: ( x in dom u implies (rngs u) . x c= a . x )
assume  x in dom u ; ::_thesis: (rngs u) . x c= a . x
then reconsider i = x as Element of dom a by A2, Th12;
 (rngs u) . i = rng (u . i) by A2, A3, FUNCT_6:22;
hence  (rngs u) . x c= a . x by RELAT_1:def_19; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_u_holds_
(doms_u)_._x_=_a_._x
let x be set ; ::_thesis: ( x in dom u implies (doms u) . x = a . x )
assume  x in dom u ; ::_thesis: (doms u) . x = a . x
then reconsider i = x as Element of dom a by A2, Th12;
(doms u) . i = dom (u . i) by A2, A3, FUNCT_6:22
.= a . i by FUNCT_2:def_1 ;
hence  (doms u) . x = a . x ; ::_thesis: verum
end;
hence  doms u = a by A2, A3, A5, FUNCT_1:2; ::_thesis: product (rngs u) c= product a
 dom (rngs u) = u " (SubFuncs (rng u)) by FUNCT_6:def_3;
hence  product (rngs u) c= product a by A1, A2, A3, A5, A6, CARD_3:27; ::_thesis: verum
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
A1: ( product (rngs u) c= product a & rng (Frege u) = product (rngs u) ) by Th14, FUNCT_6:38;
 ( dom (Frege u) = product (doms u) & doms u = a ) by Th14, FUNCT_6:def_7;
hence  Frege u is UnOp of (product a) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
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)
proof
let a be Domain-Sequence; ::_thesis: 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)
let u be UnOps of a; ::_thesis: for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let f be Element of product a; ::_thesis: for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let i be Element of dom a; ::_thesis: ((Frege u) . f) . i = (u . i) . (f . i)
A1: ( dom u = Seg (len u) & doms u = a ) by Th14, FINSEQ_1:def_3;
 ( dom a = Seg (len a) & len a = len u ) by Th12, FINSEQ_1:def_3;
hence  ((Frege u) . f) . i = (u . i) . (f . i) by A1, FUNCT_6:37; ::_thesis: verum
end;

definition
let F be functional non empty set ;
let b be BinOp of F;
let f, g be Element of F;
:: original: .
redefine funcb . (f,g) ->  Element of F;
coherence
 b . (f,g) is Element of F
proof
 b . (f,g) is Element of F ;
hence  b . (f,g) is Element of F ; ::_thesis: verum
end;
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
proof
let a be Domain-Sequence; ::_thesis: 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
let d, d9 be BinOp of (product a); ::_thesis: ( ( for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) implies d = d9 )
assume A1: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ; ::_thesis: d = d9
now__::_thesis:_for_f,_g_being_Element_of_product_a_holds_d_._(f,g)_=_d9_._(f,g)
let f, g be Element of product a; ::_thesis: d . (f,g) = d9 . (f,g)
A2: ( dom (d . (f,g)) = dom a & dom (d9 . (f,g)) = dom a ) by CARD_3:9;
 for x being set st x in dom a holds
(d . (f,g)) . x = (d9 . (f,g)) . x by A1;
hence  d . (f,g) = d9 . (f,g) by A2, FUNCT_1:2; ::_thesis: verum
end;
hence  d = d9 by BINOP_1:2; ::_thesis: verum
end;

definition
let a be Domain-Sequence;
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
 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
defpred S1[ Element of product a, Element of product a, Element of product a] means  for i being Element of dom a holds $3 . i = (b . i) . (($1 . i),($2 . i));
A1: for f, g being Element of product a ex z being Element of product a st S1[f,g,z]
proof
let f, g be Element of product a; ::_thesis: ex z being Element of product a st S1[f,g,z]
defpred S2[ set , set ] means  ex i being Element of dom a st
( $1 = i & $2 = (b . i) . ((f . i),(g . i)) );
A2: for x being set st x in dom a holds
ex z being set st S2[x,z]
proof
let x be set ; ::_thesis: ( x in dom a implies ex z being set st S2[x,z] )
assume  x in dom a ; ::_thesis: ex z being set st S2[x,z]
then reconsider i = x as Element of dom a ;
take  (b . i) . ((f . i),(g . i)) ; ::_thesis: S2[x,(b . i) . ((f . i),(g . i))]
thus  S2[x,(b . i) . ((f . i),(g . i))] ; ::_thesis: verum
end;
consider z being Function such that
A3: ( dom z = dom a & ( for x being set st x in dom a holds
S2[x,z . x] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_
z_._x_in_a_._x
let x be set ; ::_thesis: ( x in dom a implies z . x in a . x )
assume  x in dom a ; ::_thesis: z . x in a . x
then  ex i being Element of dom a st
( x = i & z . x = (b . i) . ((f . i),(g . i)) ) by A3;
hence  z . x in a . x ; ::_thesis: verum
end;
then reconsider z9 = z as Element of product a by A3, CARD_3:9;
take  z9 ; ::_thesis: S1[f,g,z9]
let i be Element of dom a; ::_thesis: z9 . i = (b . i) . ((f . i),(g . i))
 ex j being Element of dom a st
( j = i & z . i = (b . j) . ((f . j),(g . j)) ) by A3;
hence  z9 . i = (b . i) . ((f . i),(g . i)) ; ::_thesis: verum
end;
consider d being BinOp of (product a) such that
A4: for f, g being Element of product a holds S1[f,g,d . (f,g)] from BINOP_1:sch_3(A1);
take  d ; ::_thesis: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))
thus  for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A4; ::_thesis: verum
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
let d, d9 be BinOp of (product a); ::_thesis: ( ( for f, g being Element of product a
for i being Element of dom a holds (d . (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 (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) implies d = d9 )
assume that
A5: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) and
A6: for f, g being Element of product a
for i being Element of dom a holds (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ; ::_thesis: d = d9
now__::_thesis:_for_f,_g_being_Element_of_product_a
for_i_being_Element_of_dom_a_holds_(d_._(f,g))_._i_=_(d9_._(f,g))_._i
let f, g be Element of product a; ::_thesis: for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i
let i be Element of dom a; ::_thesis: (d . (f,g)) . i = (d9 . (f,g)) . i
thus (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A5
.= (d9 . (f,g)) . i by A6 ; ::_thesis: verum
end;
hence  d = d9 by Th16; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines [: PRVECT_1:def_8_:_
 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 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
proof
let a be Domain-Sequence; ::_thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative
let b be BinOps of a; ::_thesis: ( ( for i being Element of dom a holds b . i is commutative ) implies [:b:] is commutative )
assume A1: for i being Element of dom a holds b . i is commutative ; ::_thesis: [:b:] is commutative
let x, y be Element of product a; :: according to BINOP_1:def_2 ::_thesis: [:b:] . (x,y) = [:b:] . (y,x)
A2: now__::_thesis:_for_z_being_set_st_z_in_dom_a_holds_
([:b:]_._(x,y))_._z_=_([:b:]_._(y,x))_._z
let z be set ; ::_thesis: ( z in dom a implies ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z )
assume  z in dom a ; ::_thesis: ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z
then reconsider i = z as Element of dom a ;
A3: ([:b:] . (y,x)) . i = (b . i) . ((y . i),(x . i)) by Def8;
 ( b . i is commutative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence  ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z by A3, BINOP_1:def_2; ::_thesis: verum
end;
 ( dom ([:b:] . (x,y)) = dom a & dom ([:b:] . (y,x)) = dom a ) by CARD_3:9;
hence  [:b:] . (x,y) = [:b:] . (y,x) by A2, FUNCT_1:2; ::_thesis: verum
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
proof
let a be Domain-Sequence; ::_thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative
let b be BinOps of a; ::_thesis: ( ( for i being Element of dom a holds b . i is associative ) implies [:b:] is associative )
assume A1: for i being Element of dom a holds b . i is associative ; ::_thesis: [:b:] is associative
let x, y, z be Element of product a; :: according to BINOP_1:def_3 ::_thesis: [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z)
A2: now__::_thesis:_for_v_being_set_st_v_in_dom_a_holds_
([:b:]_._(x,([:b:]_._(y,z))))_._v_=_([:b:]_._(([:b:]_._(x,y)),z))_._v
set xy = [:b:] . (x,y);
set yz = [:b:] . (y,z);
let v be set ; ::_thesis: ( v in dom a implies ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v )
assume  v in dom a ; ::_thesis: ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v
then reconsider i = v as Element of dom a ;
A3: ( ([:b:] . (y,z)) . i = (b . i) . ((y . i),(z . i)) & ([:b:] . (x,([:b:] . (y,z)))) . i = (b . i) . ((x . i),(([:b:] . (y,z)) . i)) ) by Def8;
A4: ([:b:] . (([:b:] . (x,y)),z)) . i = (b . i) . ((([:b:] . (x,y)) . i),(z . i)) by Def8;
 ( b . i is associative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence  ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v by A3, A4, BINOP_1:def_3; ::_thesis: verum
end;
 ( dom ([:b:] . (x,([:b:] . (y,z)))) = dom a & dom ([:b:] . (([:b:] . (x,y)),z)) = dom a ) by CARD_3:9;
hence  [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z) by A2, FUNCT_1:2; ::_thesis: verum
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:]
proof
let a be Domain-Sequence; ::_thesis: 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:]
let b be BinOps of a; ::_thesis: 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:]
let f be Element of product a; ::_thesis: ( ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) implies f is_a_unity_wrt [:b:] )
assume A1: for i being Element of dom a holds f . i is_a_unity_wrt b . i ; ::_thesis: f is_a_unity_wrt [:b:]
now__::_thesis:_for_x_being_Element_of_product_a_holds_
(_[:b:]_._(f,x)_=_x_&_[:b:]_._(x,f)_=_x_)
let x be Element of product a; ::_thesis: ( [:b:] . (f,x) = x & [:b:] . (x,f) = x )
A2: dom x = dom a by CARD_3:9;
A3: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(f,x))_._y_=_x_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (f,x)) . y = x . y )
assume  y in dom a ; ::_thesis: ([:b:] . (f,x)) . y = x . y
then reconsider i = y as Element of dom a ;
 ( ([:b:] . (f,x)) . i = (b . i) . ((f . i),(x . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence  ([:b:] . (f,x)) . y = x . y by BINOP_1:3; ::_thesis: verum
end;
 dom ([:b:] . (f,x)) = dom a by CARD_3:9;
hence  [:b:] . (f,x) = x by A2, A3, FUNCT_1:2; ::_thesis: [:b:] . (x,f) = x
A4: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(x,f))_._y_=_x_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (x,f)) . y = x . y )
assume  y in dom a ; ::_thesis: ([:b:] . (x,f)) . y = x . y
then reconsider i = y as Element of dom a ;
 ( ([:b:] . (x,f)) . i = (b . i) . ((x . i),(f . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence  ([:b:] . (x,f)) . y = x . y by BINOP_1:3; ::_thesis: verum
end;
 dom ([:b:] . (x,f)) = dom a by CARD_3:9;
hence  [:b:] . (x,f) = x by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
hence  f is_a_unity_wrt [:b:] by BINOP_1:3; ::_thesis: verum
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:]
proof
let a be Domain-Sequence; ::_thesis: 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:]
let b be BinOps of a; ::_thesis: 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:]
let u be UnOps of a; ::_thesis: ( ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) implies Frege u is_an_inverseOp_wrt [:b:] )
assume A1: for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ; ::_thesis: Frege u is_an_inverseOp_wrt [:b:]
defpred S1[ set , set ] means  ex i being Element of dom a st
( $1 = i & $2 = the_unity_wrt (b . i) );
A2: for x being set st x in dom a holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom a implies ex y being set st S1[x,y] )
assume  x in dom a ; ::_thesis: ex y being set st S1[x,y]
then reconsider i = x as Element of dom a ;
take  the_unity_wrt (b . i) ; ::_thesis: S1[x, the_unity_wrt (b . i)]
thus  S1[x, the_unity_wrt (b . i)] ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = dom a & ( for x being set st x in dom a holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_
f_._x_in_a_._x
let x be set ; ::_thesis: ( x in dom a implies f . x in a . x )
assume  x in dom a ; ::_thesis: f . x in a . x
then  ex i being Element of dom a st
( x = i & f . x = the_unity_wrt (b . i) ) by A3;
hence  f . x in a . x ; ::_thesis: verum
end;
then reconsider f = f as Element of product a by A3, CARD_3:9;
let x be Element of product a; :: according to FINSEQOP:def_1 ::_thesis: ( [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] & [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] )
A4: dom f = dom a by CARD_3:9;
A5: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(x,((Frege_u)_._x)))_._y_=_f_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (x,((Frege u) . x))) . y = f . y )
assume  y in dom a ; ::_thesis: ([:b:] . (x,((Frege u) . x))) . y = f . y
then reconsider i = y as Element of dom a ;
A6: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
 ( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (x,((Frege u) . x))) . i = (b . i) . ((x . i),(((Frege u) . x) . i)) ) by A3, Def8;
hence  ([:b:] . (x,((Frege u) . x))) . y = f . y by A6, FINSEQOP:def_1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_a_holds_f_._i_is_a_unity_wrt_b_._i
let i be Element of dom a; ::_thesis: f . i is_a_unity_wrt b . i
 ( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & b . i is having_a_unity ) by A1, A3;
hence  f . i is_a_unity_wrt b . i by SETWISEO:14; ::_thesis: verum
end;
then  f is_a_unity_wrt [:b:] by Th19;
then A7: f = the_unity_wrt [:b:] by BINOP_1:def_8;
A8: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(((Frege_u)_._x),x))_._y_=_f_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (((Frege u) . x),x)) . y = f . y )
assume  y in dom a ; ::_thesis: ([:b:] . (((Frege u) . x),x)) . y = f . y
then reconsider i = y as Element of dom a ;
A9: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
 ( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (((Frege u) . x),x)) . i = (b . i) . ((((Frege u) . x) . i),(x . i)) ) by A3, Def8;
hence  ([:b:] . (((Frege u) . x),x)) . y = f . y by A9, FINSEQOP:def_1; ::_thesis: verum
end;
 dom ([:b:] . (x,((Frege u) . x))) = dom a by CARD_3:9;
hence  [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] by A7, A4, A5, FUNCT_1:2; ::_thesis: [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:]
 dom ([:b:] . (((Frege u) . x),x)) = dom a by CARD_3:9;
hence  [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] by A7, A4, A8, FUNCT_1:2; ::_thesis: verum
end;

begin

definition
let F be Relation;
attrF is AbGroup-yielding  means :Def9: :: PRVECT_1:def 9
 for x being set st x in rng F holds
x is AbGroup;
end;

:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def_9_:_
 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 Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like AbGroup-yielding for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty & b1 is AbGroup-yielding )
proof
set A = the AbGroup;
take  <* the AbGroup*> ; ::_thesis: ( not <* the AbGroup*> is empty & <* the AbGroup*> is AbGroup-yielding )
thus  not <* the AbGroup*> is empty ; ::_thesis: <* the AbGroup*> is AbGroup-yielding
let x be set ; :: according to PRVECT_1:def_9 ::_thesis: ( x in rng <* the AbGroup*> implies x is AbGroup )
assume that
A1: x in rng <* the AbGroup*> and
A2: x is not AbGroup ; ::_thesis: contradiction
 x in { the AbGroup} by A1, FINSEQ_1:38;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
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 funcg . i ->  AbGroup;
coherence
 g . i is AbGroup
proof
 g . i in rng g by FUNCT_1:def_3;
hence  g . i is AbGroup by Def9; ::_thesis: verum
end;
end;

definition
let g be Group-Sequence;
func carr g ->  Domain-Sequence means :Def10: :: PRVECT_1:def 10
( 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
defpred S1[ set , set ] means  ex j9 being Element of dom g st
( j9 = $1 & $2 = the carrier of (g . j9) );
A1: for j being Nat st j in Seg (len g) holds
ex x being set st S1[j,x]
proof
let j be Nat; ::_thesis: ( j in Seg (len g) implies ex x being set st S1[j,x] )
assume  j in Seg (len g) ; ::_thesis: ex x being set st S1[j,x]
then reconsider j9 = j as Element of dom g by FINSEQ_1:def_3;
take  the carrier of (g . j9) ; ::_thesis: S1[j, the carrier of (g . j9)]
thus  S1[j, the carrier of (g . j9)] ; ::_thesis: verum
end;
consider p being FinSequence such that
A2: ( dom p = Seg (len g) & ( for j being Nat st j in Seg (len g) holds
S1[j,p . j] ) ) from FINSEQ_1:sch_1(A1);
 p is non-empty
proof
assume  {} in rng p ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then consider x being set  such that
A3: x in dom p and
A4: {} = p . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
 ex x9 being Element of dom g st
( x9 = x & p . x = the carrier of (g . x9) ) by A2, A3;
hence  contradiction by A4; ::_thesis: verum
end;
then reconsider p9 = p as Domain-Sequence by A2;
take  p9 ; ::_thesis: ( len p9 = len g & ( for j being Element of dom g holds p9 . j = the carrier of (g . j) ) )
thus  len p9 = len g by A2, FINSEQ_1:def_3; ::_thesis: for j being Element of dom g holds p9 . j = the carrier of (g . j)
let j be Element of dom g; ::_thesis: p9 . j = the carrier of (g . j)
reconsider k = j as Element of NAT ;
 dom g = Seg (len g) by FINSEQ_1:def_3;
then  ex j9 being Element of dom g st
( j9 = k & p9 . k = the carrier of (g . j9) ) by A2;
hence  p9 . j = the carrier of (g . j) ; ::_thesis: verum
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
let f, h be Domain-Sequence; ::_thesis: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) & len h = len g & ( for j being Element of dom g holds h . j = the carrier of (g . j) ) implies f = h )
assume that
A5: len f = len g and
A6: for j being Element of dom g holds f . j = the carrier of (g . j) and
A7: len h = len g and
A8: for j being Element of dom g holds h . j = the carrier of (g . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_f9_holds_
f9_._j_=_h9_._j
let j be Nat; ::_thesis: ( j in dom f9 implies f9 . j = h9 . j )
assume  j in dom f9 ; ::_thesis: f9 . j = h9 . j
then reconsider j9 = j as Element of dom g by A5, FINSEQ_3:29;
 f9 . j = the carrier of (g . j9) by A6;
hence  f9 . j = h9 . j by A8; ::_thesis: verum
end;
 ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence  f = h by A5, A7, A9, FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines carr PRVECT_1:def_10_:_
 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 funcg . i ->  AbGroup;
coherence
 g . i is AbGroup
proof
 ( dom g = Seg (len g) & Seg (len (carr g)) = dom (carr g) ) by FINSEQ_1:def_3;
then reconsider i9 = i as Element of dom g by Def10;
 g . i9 is AbGroup ;
hence  g . i is AbGroup ; ::_thesis: verum
end;
end;

definition
let g be Group-Sequence;
func addop g ->  BinOps of carr g means :Def11: :: PRVECT_1:def 11
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF 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 addF of (g . i) ) )
proof
deffunc H5( Element of dom (carr g)) ->  Element of bool [:[: the carrier of (g . $1), the carrier of (g . $1):], the carrier of (g . $1):] = the addF of (g . $1);
consider p being non empty FinSequence such that
A1: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_i_being_Element_of_dom_(carr_g)_holds_p_._i_is_BinOp_of_((carr_g)_._i)
let i be Element of dom (carr g); ::_thesis: p . i is BinOp of ((carr g) . i)
 len g = len (carr g) by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
 ( p . i = the addF of (g . i) & the carrier of (g . j) = (carr g) . j ) by A1, Def10;
hence  p . i is BinOp of ((carr g) . i) ; ::_thesis: verum
end;
then reconsider p9 = p as BinOps of carr g by A1, Th11;
take  p9 ; ::_thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) )
thus  ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) ) by A1; ::_thesis: verum
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 addF of (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the addF of (g . i) ) holds
b1 = b2
proof
let f, h be BinOps of carr g; ::_thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = the addF of (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = the addF of (g . i) ) implies f = h )
assume that
A2: len f = len (carr g) and
A3: for i being Element of dom (carr g) holds f . i = the addF of (g . i) and
A4: len h = len (carr g) and
A5: for i being Element of dom (carr g) holds h . i = the addF of (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f9_._i_=_h9_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i )
assume  i in dom f9 ; ::_thesis: f9 . i = h9 . i
then reconsider i9 = i as Element of dom (carr g) by A2, FINSEQ_3:29;
 f9 . i = the addF of (g . i9) by A3;
hence  f9 . i = h9 . i by A5; ::_thesis: verum
end;
 ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence  f = h by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum
end;
func complop g ->  UnOps of carr g means :Def12: :: PRVECT_1:def 12
( 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
deffunc H5( Element of dom (carr g)) ->  Element of bool [: the carrier of (g . $1), the carrier of (g . $1):] = comp (g . $1);
consider p being non empty FinSequence such that
A7: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_i_being_Element_of_dom_(carr_g)_holds_p_._i_is_UnOp_of_((carr_g)_._i)
let i be Element of dom (carr g); ::_thesis: p . i is UnOp of ((carr g) . i)
 len g = len (carr g) by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
 ( p . i = comp (g . i) & the carrier of (g . j) = (carr g) . j ) by A7, Def10;
hence  p . i is UnOp of ((carr g) . i) ; ::_thesis: verum
end;
then reconsider p9 = p as UnOps of carr g by A7, Th12;
take  p9 ; ::_thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) )
thus  ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) ) by A7; ::_thesis: verum
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
let f, h be UnOps of carr g; ::_thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = comp (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = comp (g . i) ) implies f = h )
assume that
A8: len f = len (carr g) and
A9: for i being Element of dom (carr g) holds f . i = comp (g . i) and
A10: len h = len (carr g) and
A11: for i being Element of dom (carr g) holds h . i = comp (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f_._i_=_h_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f . i = h . i )
assume  i in dom f9 ; ::_thesis: f . i = h . i
then reconsider i9 = i as Element of dom (carr g) by A8, FINSEQ_3:29;
 f . i = comp (g . i9) by A9;
hence  f . i = h . i by A11; ::_thesis: verum
end;
 ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence  f = h by A8, A10, A12, FINSEQ_1:13; ::_thesis: verum
end;
func zeros g ->  Element of product (carr g) means :Def13: :: PRVECT_1:def 13
 for i being Element of dom (carr g) holds it . i = 0. (g . i);
existence
 ex b1 being Element of product (carr g) st
for i being Element of dom (carr g) holds b1 . i = 0. (g . i)
proof
deffunc H5( Element of dom (carr g)) ->  Element of the carrier of (g . $1) = 0. (g . $1);
A13: dom (carr g) = Seg (len (carr g)) by FINSEQ_1:def_3;
consider p being non empty FinSequence such that
A14: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
A15: dom g = Seg (len g) by FINSEQ_1:def_3;
A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_g)_holds_
p_._i_in_(carr_g)_._i
let i be set ; ::_thesis: ( i in dom (carr g) implies p . i in (carr g) . i )
assume  i in dom (carr g) ; ::_thesis: p . i in (carr g) . i
then reconsider x = i as Element of dom (carr g) ;
reconsider x9 = x as Element of dom g by A15, A13, Def10;
 ( p . x = 0. (g . x) & (carr g) . x9 = the carrier of (g . x9) ) by A14, Def10;
hence  p . i in (carr g) . i ; ::_thesis: verum
end;
 dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider t = p as Element of product (carr g) by A14, A13, A16, CARD_3:9;
take  t ; ::_thesis: for i being Element of dom (carr g) holds t . i = 0. (g . i)
thus  for i being Element of dom (carr g) holds t . i = 0. (g . i) by A14; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of product (carr g) st ( for i being Element of dom (carr g) holds b1 . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds b2 . i = 0. (g . i) ) holds
b1 = b2
proof
let f, h be Element of product (carr g); ::_thesis: ( ( for i being Element of dom (carr g) holds f . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds h . i = 0. (g . i) ) implies f = h )
assume that
A17: for i being Element of dom (carr g) holds f . i = 0. (g . i) and
A18: for i being Element of dom (carr g) holds h . i = 0. (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as Function ;
A19: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_g)_holds_
f9_._x_=_h9_._x
let x be set ; ::_thesis: ( x in dom (carr g) implies f9 . x = h9 . x )
assume  x in dom (carr g) ; ::_thesis: f9 . x = h9 . x
then reconsider i = x as Element of dom (carr g) ;
thus f9 . x = 0. (g . i) by A17
.= h9 . x by A18 ; ::_thesis: verum
end;
 ( dom f9 = dom (carr g) & dom h9 = dom (carr g) ) by CARD_3:9;
hence  f = h by A19, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines addop PRVECT_1:def_11_:_
 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 addF of (g . i) ) ) );

:: deftheorem Def12 defines complop PRVECT_1:def_12_:_
 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 Def13 defines zeros PRVECT_1:def_13_:_
 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 = 0. (g . i) );

definition
let G be Group-Sequence;
func product G ->  strict AbGroup equals :: PRVECT_1:def 14
 addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence
 addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup
proof
reconsider GS = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) as non empty addLoopStr ;
A1: now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(carr_G)_._i_=_H1(G_._i)
let i be Element of dom (carr G); ::_thesis: (carr G) . i = H1(G . i)
dom G = Seg (len G) by FINSEQ_1:def_3
.= Seg (len (carr G)) by Def10
.= dom (carr G) by FINSEQ_1:def_3 ;
hence  (carr G) . i = H1(G . i) by Def10; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_associative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is associative
 ( (addop G) . i = H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Def11;
hence  (addop G) . i is associative by FVSUM_1:2; ::_thesis: verum
end;
then A2: [:(addop G):] is associative by Th18;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(zeros_G)_._i_is_a_unity_wrt_(addop_G)_._i
let i be Element of dom (carr G); ::_thesis: (zeros G) . i is_a_unity_wrt (addop G) . i
A3: (carr G) . i = H1(G . i) by A1;
 ( (addop G) . i = H2(G . i) & (zeros G) . i = H4(G . i) ) by Def11, Def13;
hence  (zeros G) . i is_a_unity_wrt (addop G) . i by A3, Th1; ::_thesis: verum
end;
then A4: zeros G is_a_unity_wrt [:(addop G):] by Th19;
A5: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. GS
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_
(_(complop_G)_._i_is_an_inverseOp_wrt_(addop_G)_._i_&_(addop_G)_._i_is_having_a_unity_)
let i be Element of dom (carr G); ::_thesis: ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )
A6: ( (addop G) . i = H2(G . i) & (complop G) . i = H3(G . i) ) by Def11, Def12;
 ( H4(G . i) is_a_unity_wrt H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Th1;
hence  ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, Th2, SETWISEO:def_2; ::_thesis: verum
end;
then  Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by Th20;
then  x + y = the_unity_wrt [:(addop G):] by FINSEQOP:def_1;
hence  x + y = 0. GS by A4, BINOP_1:def_8; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_commutative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is commutative
 ( (addop G) . i = H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Def11;
hence  (addop G) . i is commutative by FVSUM_1:1; ::_thesis: verum
end;
then  ( 0. GS = zeros G & [:(addop G):] is commutative ) by Th17;
hence  addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup by A2, A4, A5, Lm2, Lm3; ::_thesis: verum
end;
end;

:: deftheorem  defines product PRVECT_1:def_14_:_
 for G being Group-Sequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);