:: by Artur Korni{\l}owicz

::

:: Received June 10, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

definition

let R be Relation;

end;
attr R is multMagma-yielding means :Def1: :: GROUP_7:def 1

for y being set st y in rng R holds

y is non empty multMagma ;

for y being set st y in rng R holds

y is non empty multMagma ;

:: deftheorem Def1 defines multMagma-yielding GROUP_7:def 1 :

for R being Relation holds

( R is multMagma-yielding iff for y being set st y in rng R holds

y is non empty multMagma );

for R being Relation holds

( R is multMagma-yielding iff for y being set st y in rng R holds

y is non empty multMagma );

registration

coherence

for b_{1} being Function st b_{1} is multMagma-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st b_{1} is multMagma-yielding

end;
existence

ex b

proof end;

definition

let I be non empty set ;

let F be multMagma-Family of I;

let i be Element of I;

:: original: .

redefine func F . i -> non empty multMagma ;

coherence

F . i is non empty multMagma

end;
let F be multMagma-Family of I;

let i be Element of I;

:: original: .

redefine func F . i -> non empty multMagma ;

coherence

F . i is non empty multMagma

proof end;

registration
end;

Lm1: now :: thesis: for I being non empty set

for i being Element of I

for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

for i being Element of I

for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let I be non empty set ; :: thesis: for i being Element of I

for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let i be Element of I; :: thesis: for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let F be multMagma-yielding ManySortedSet of I; :: thesis: for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let f be Element of product (Carrier F); :: thesis: f . i in the carrier of (F . i)

A1: dom (Carrier F) = I by PARTFUN1:def 2;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;

hence f . i in the carrier of (F . i) by A1, CARD_3:9; :: thesis: verum

end;
for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let i be Element of I; :: thesis: for F being multMagma-yielding ManySortedSet of I

for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let F be multMagma-yielding ManySortedSet of I; :: thesis: for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)

let f be Element of product (Carrier F); :: thesis: f . i in the carrier of (F . i)

A1: dom (Carrier F) = I by PARTFUN1:def 2;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;

hence f . i in the carrier of (F . i) by A1, CARD_3:9; :: thesis: verum

definition

let I be set ;

let F be multMagma-Family of I;

ex b_{1} being strict multMagma st

( the carrier of b_{1} = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b_{1} . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )

for b_{1}, b_{2} being strict multMagma st the carrier of b_{1} = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b_{1} . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of b_{2} = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b_{2} . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) holds

b_{1} = b_{2}

end;
let F be multMagma-Family of I;

func product F -> strict multMagma means :Def2: :: GROUP_7:def 2

( the carrier of it = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of it . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) );

existence ( the carrier of it = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of it . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) );

ex b

( the carrier of b

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b

proof end;

uniqueness for b

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b

b

proof end;

:: deftheorem Def2 defines product GROUP_7:def 2 :

for I being set

for F being multMagma-Family of I

for b_{3} being strict multMagma holds

( b_{3} = product F iff ( the carrier of b_{3} = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b_{3} . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) );

for I being set

for F being multMagma-Family of I

for b

( b

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of b

registration

let I be set ;

let F be multMagma-Family of I;

coherence

( not product F is empty & product F is constituted-Functions )

end;
let F be multMagma-Family of I;

coherence

( not product F is empty & product F is constituted-Functions )

proof end;

theorem Th1: :: GROUP_7:1

for i, I being set

for f, g, h being Function

for F being multMagma-Family of I

for G being non empty multMagma

for p, q being Element of (product F)

for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds

x * y = h . i

for f, g, h being Function

for F being multMagma-Family of I

for G being non empty multMagma

for p, q being Element of (product F)

for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds

x * y = h . i

proof end;

definition

let I be set ;

let F be multMagma-Family of I;

end;
let F be multMagma-Family of I;

attr F is Group-like means :Def3: :: GROUP_7:def 3

for i being set st i in I holds

ex Fi being non empty Group-like multMagma st Fi = F . i;

for i being set st i in I holds

ex Fi being non empty Group-like multMagma st Fi = F . i;

attr F is associative means :Def4: :: GROUP_7:def 4

for i being set st i in I holds

ex Fi being non empty associative multMagma st Fi = F . i;

for i being set st i in I holds

ex Fi being non empty associative multMagma st Fi = F . i;

attr F is commutative means :Def5: :: GROUP_7:def 5

for i being set st i in I holds

ex Fi being non empty commutative multMagma st Fi = F . i;

for i being set st i in I holds

ex Fi being non empty commutative multMagma st Fi = F . i;

:: deftheorem Def3 defines Group-like GROUP_7:def 3 :

for I being set

for F being multMagma-Family of I holds

( F is Group-like iff for i being set st i in I holds

ex Fi being non empty Group-like multMagma st Fi = F . i );

for I being set

for F being multMagma-Family of I holds

( F is Group-like iff for i being set st i in I holds

ex Fi being non empty Group-like multMagma st Fi = F . i );

:: deftheorem Def4 defines associative GROUP_7:def 4 :

for I being set

for F being multMagma-Family of I holds

( F is associative iff for i being set st i in I holds

ex Fi being non empty associative multMagma st Fi = F . i );

for I being set

for F being multMagma-Family of I holds

( F is associative iff for i being set st i in I holds

ex Fi being non empty associative multMagma st Fi = F . i );

:: deftheorem Def5 defines commutative GROUP_7:def 5 :

for I being set

for F being multMagma-Family of I holds

( F is commutative iff for i being set st i in I holds

ex Fi being non empty commutative multMagma st Fi = F . i );

for I being set

for F being multMagma-Family of I holds

( F is commutative iff for i being set st i in I holds

ex Fi being non empty commutative multMagma st Fi = F . i );

definition

let I be non empty set ;

let F be multMagma-Family of I;

( F is Group-like iff for i being Element of I holds F . i is Group-like )

( F is associative iff for i being Element of I holds F . i is associative )

( F is commutative iff for i being Element of I holds F . i is commutative )

end;
let F be multMagma-Family of I;

redefine attr F is Group-like means :Def6: :: GROUP_7:def 6

for i being Element of I holds F . i is Group-like ;

compatibility for i being Element of I holds F . i is Group-like ;

( F is Group-like iff for i being Element of I holds F . i is Group-like )

proof end;

redefine attr F is associative means :Def7: :: GROUP_7:def 7

for i being Element of I holds F . i is associative ;

compatibility for i being Element of I holds F . i is associative ;

( F is associative iff for i being Element of I holds F . i is associative )

proof end;

redefine attr F is commutative means :: GROUP_7:def 8

for i being Element of I holds F . i is commutative ;

compatibility for i being Element of I holds F . i is commutative ;

( F is commutative iff for i being Element of I holds F . i is commutative )

proof end;

:: deftheorem Def6 defines Group-like GROUP_7:def 6 :

for I being non empty set

for F being multMagma-Family of I holds

( F is Group-like iff for i being Element of I holds F . i is Group-like );

for I being non empty set

for F being multMagma-Family of I holds

( F is Group-like iff for i being Element of I holds F . i is Group-like );

:: deftheorem Def7 defines associative GROUP_7:def 7 :

for I being non empty set

for F being multMagma-Family of I holds

( F is associative iff for i being Element of I holds F . i is associative );

for I being non empty set

for F being multMagma-Family of I holds

( F is associative iff for i being Element of I holds F . i is associative );

:: deftheorem defines commutative GROUP_7:def 8 :

for I being non empty set

for F being multMagma-Family of I holds

( F is commutative iff for i being Element of I holds F . i is commutative );

for I being non empty set

for F being multMagma-Family of I holds

( F is commutative iff for i being Element of I holds F . i is commutative );

registration

let I be set ;

ex b_{1} being multMagma-Family of I st

( b_{1} is Group-like & b_{1} is associative & b_{1} is commutative )

end;
cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative commutative for set ;

existence ex b

( b

proof end;

registration

let I be set ;

let F be Group-like multMagma-Family of I;

coherence

product F is Group-like

end;
let F be Group-like multMagma-Family of I;

coherence

product F is Group-like

proof end;

registration

let I be set ;

let F be associative multMagma-Family of I;

coherence

product F is associative

end;
let F be associative multMagma-Family of I;

coherence

product F is associative

proof end;

registration

let I be set ;

let F be commutative multMagma-Family of I;

coherence

product F is commutative

end;
let F be commutative multMagma-Family of I;

coherence

product F is commutative

proof end;

theorem :: GROUP_7:2

for i, I being set

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

proof end;

theorem :: GROUP_7:3

for i, I being set

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is associative holds

G is associative

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is associative holds

G is associative

proof end;

theorem :: GROUP_7:4

for i, I being set

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is commutative holds

G is commutative

for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is commutative holds

G is commutative

proof end;

theorem Th5: :: GROUP_7:5

for I being set

for s being ManySortedSet of I

for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

for s being ManySortedSet of I

for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

proof end;

theorem Th6: :: GROUP_7:6

for i, I being set

for f being Function

for F being Group-like multMagma-Family of I

for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds

f . i = 1_ G

for f being Function

for F being Group-like multMagma-Family of I

for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds

f . i = 1_ G

proof end;

theorem Th7: :: GROUP_7:7

for I being set

for g being Function

for s being ManySortedSet of I

for F being Group-like associative multMagma-Family of I

for x being Element of (product F) st x = g & ( for i being set st i in I holds

ex G being Group ex y being Element of G st

( G = F . i & s . i = y " & y = g . i ) ) holds

s = x "

for g being Function

for s being ManySortedSet of I

for F being Group-like associative multMagma-Family of I

for x being Element of (product F) st x = g & ( for i being set st i in I holds

ex G being Group ex y being Element of G st

( G = F . i & s . i = y " & y = g . i ) ) holds

s = x "

proof end;

theorem Th8: :: GROUP_7:8

for i, I being set

for f, g being Function

for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

for f, g being Function

for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

proof end;

definition

let I be set ;

let F be Group-like associative multMagma-Family of I;

ex b_{1} being strict Subgroup of product F st

for x being object holds

( x in the carrier of b_{1} iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )

for b_{1}, b_{2} being strict Subgroup of product F st ( for x being object holds

( x in the carrier of b_{1} iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being object holds

( x in the carrier of b_{2} iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) holds

b_{1} = b_{2}

end;
let F be Group-like associative multMagma-Family of I;

func sum F -> strict Subgroup of product F means :Def9: :: GROUP_7:def 9

for x being object holds

( x in the carrier of it iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) );

existence for x being object holds

( x in the carrier of it iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) );

ex b

for x being object holds

( x in the carrier of b

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )

proof end;

uniqueness for b

( x in the carrier of b

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being object holds

( x in the carrier of b

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) holds

b

proof end;

:: deftheorem Def9 defines sum GROUP_7:def 9 :

for I being set

for F being Group-like associative multMagma-Family of I

for b_{3} being strict Subgroup of product F holds

( b_{3} = sum F iff for x being object holds

( x in the carrier of b_{3} iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) );

for I being set

for F being Group-like associative multMagma-Family of I

for b

( b

( x in the carrier of b

( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds

ex G being non empty Group-like multMagma st

( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) );

registration

let I be set ;

let F be Group-like associative multMagma-Family of I;

let f, g be Element of (sum F);

coherence

( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like )

end;
let F be Group-like associative multMagma-Family of I;

let f, g be Element of (sum F);

coherence

( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like )

proof end;

theorem :: GROUP_7:9

for I being finite set

for F being Group-like associative multMagma-Family of I holds product F = sum F

for F being Group-like associative multMagma-Family of I holds product F = sum F

proof end;

registration

let G1 be non empty multMagma ;

coherence

( <*G1*> is total & <*G1*> is multMagma-yielding ) by Th10;

end;
coherence

( <*G1*> is total & <*G1*> is multMagma-yielding ) by Th10;

registration
end;

registration
end;

registration
end;

theorem :: GROUP_7:14

theorem :: GROUP_7:15

for G1 being commutative Group holds <*G1*> is Group-like associative commutative multMagma-Family of {1} ;

registration

let G1 be non empty multMagma ;

coherence

for b_{1} being Element of product (Carrier <*G1*>) holds b_{1} is FinSequence-like
by FINSEQ_1:2, PARTFUN1:def 2;

end;
coherence

for b

registration

let G1 be non empty multMagma ;

coherence

for b_{1} being Element of (product <*G1*>) holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

definition

let G1 be non empty multMagma ;

let x be Element of G1;

:: original: <*

redefine func <*x*> -> Element of (product <*G1*>);

coherence

<*x*> is Element of (product <*G1*>)

end;
let x be Element of G1;

:: original: <*

redefine func <*x*> -> Element of (product <*G1*>);

coherence

<*x*> is Element of (product <*G1*>)

proof end;

registration
end;

registration

let G1, G2 be non empty multMagma ;

coherence

( <*G1,G2*> is total & <*G1,G2*> is multMagma-yielding ) by Th16;

end;
coherence

( <*G1,G2*> is total & <*G1,G2*> is multMagma-yielding ) by Th16;

theorem Th17: :: GROUP_7:17

for G1, G2 being non empty Group-like multMagma holds <*G1,G2*> is Group-like multMagma-Family of {1,2}

proof end;

registration
end;

theorem Th18: :: GROUP_7:18

for G1, G2 being non empty associative multMagma holds <*G1,G2*> is associative multMagma-Family of {1,2}

proof end;

registration
end;

theorem Th19: :: GROUP_7:19

for G1, G2 being non empty commutative multMagma holds <*G1,G2*> is commutative multMagma-Family of {1,2}

proof end;

registration
end;

theorem :: GROUP_7:20

theorem :: GROUP_7:21

for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative multMagma-Family of {1,2} ;

registration

let G1, G2 be non empty multMagma ;

coherence

for b_{1} being Element of product (Carrier <*G1,G2*>) holds b_{1} is FinSequence-like
by FINSEQ_1:2, PARTFUN1:def 2;

end;
coherence

for b

registration

let G1, G2 be non empty multMagma ;

coherence

for b_{1} being Element of (product <*G1,G2*>) holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

definition

let G1, G2 be non empty multMagma ;

let x be Element of G1;

let y be Element of G2;

:: original: <*

redefine func <*x,y*> -> Element of (product <*G1,G2*>);

coherence

<*x,y*> is Element of (product <*G1,G2*>)

end;
let x be Element of G1;

let y be Element of G2;

:: original: <*

redefine func <*x,y*> -> Element of (product <*G1,G2*>);

coherence

<*x,y*> is Element of (product <*G1,G2*>)

proof end;

registration
end;

registration

let G1, G2, G3 be non empty multMagma ;

coherence

( <*G1,G2,G3*> is total & <*G1,G2,G3*> is multMagma-yielding ) by Th22;

end;
coherence

( <*G1,G2,G3*> is total & <*G1,G2,G3*> is multMagma-yielding ) by Th22;

theorem Th23: :: GROUP_7:23

for G1, G2, G3 being non empty Group-like multMagma holds <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}

proof end;

registration
end;

theorem Th24: :: GROUP_7:24

for G1, G2, G3 being non empty associative multMagma holds <*G1,G2,G3*> is associative multMagma-Family of {1,2,3}

proof end;

registration
end;

theorem Th25: :: GROUP_7:25

for G1, G2, G3 being non empty commutative multMagma holds <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}

proof end;

registration
end;

theorem :: GROUP_7:26

for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3} ;

theorem :: GROUP_7:27

for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is Group-like associative commutative multMagma-Family of {1,2,3} ;

registration

let G1, G2, G3 be non empty multMagma ;

coherence

for b_{1} being Element of product (Carrier <*G1,G2,G3*>) holds b_{1} is FinSequence-like
by FINSEQ_3:1, PARTFUN1:def 2;

end;
coherence

for b

registration

let G1, G2, G3 be non empty multMagma ;

coherence

for b_{1} being Element of (product <*G1,G2,G3*>) holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

definition

let G1, G2, G3 be non empty multMagma ;

let x be Element of G1;

let y be Element of G2;

let z be Element of G3;

:: original: <*

redefine func <*x,y,z*> -> Element of (product <*G1,G2,G3*>);

coherence

<*x,y,z*> is Element of (product <*G1,G2,G3*>)

end;
let x be Element of G1;

let y be Element of G2;

let z be Element of G3;

:: original: <*

redefine func <*x,y,z*> -> Element of (product <*G1,G2,G3*>);

coherence

<*x,y,z*> is Element of (product <*G1,G2,G3*>)

proof end;

theorem Th28: :: GROUP_7:28

for G1 being non empty multMagma

for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>

for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>

proof end;

theorem :: GROUP_7:29

for G1, G2 being non empty multMagma

for x1, x2 being Element of G1

for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

for x1, x2 being Element of G1

for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

proof end;

theorem :: GROUP_7:30

for G1, G2, G3 being non empty multMagma

for x1, x2 being Element of G1

for y1, y2 being Element of G2

for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>

for x1, x2 being Element of G1

for y1, y2 being Element of G2

for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>

proof end;

theorem :: GROUP_7:33

for G1, G2, G3 being non empty Group-like multMagma holds 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>

proof end;

theorem :: GROUP_7:35

for G1, G2 being Group

for x being Element of G1

for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>

for x being Element of G1

for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>

proof end;

theorem :: GROUP_7:36

for G1, G2, G3 being Group

for x being Element of G1

for y being Element of G2

for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>

for x being Element of G1

for y being Element of G2

for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>

proof end;

theorem Th37: :: GROUP_7:37

for G1 being Group

for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds

f is Homomorphism of G1,(product <*G1*>)

for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds

f is Homomorphism of G1,(product <*G1*>)

proof end;

theorem Th38: :: GROUP_7:38

for G1 being Group

for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds

f is bijective

for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds

f is bijective

proof end;