set U = product (Carrier <*G,A*>);
defpred S1[ Element of product (Carrier <*G,A*>), Element of product (Carrier <*G,A*>), set ] means ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = $3 & a1 = $1 . 2 & g2 = $2 . 1 & h . 1 = the multF of G . (($1 . 1),((phi . a1) . g2)) & h . 2 = the multF of A . (($1 . 2),($2 . 2)) );
A1:
for x, y being Element of product (Carrier <*G,A*>) ex z being Element of product (Carrier <*G,A*>) st S1[x,y,z]
proof
let x,
y be
Element of
product (Carrier <*G,A*>);
ex z being Element of product (Carrier <*G,A*>) st S1[x,y,z]
y . 1
in G
by Lm1;
then reconsider g2 =
y . 1 as
Element of
G ;
x . 2
in A
by Lm1;
then reconsider a1 =
x . 2 as
Element of
A ;
set h =
<*( the multF of G . ((x . 1),((phi . a1) . g2))),( the multF of A . ((x . 2),(y . 2)))*>;
phi . a1 is
Homomorphism of
G,
G
by AUTGROUP:def 1;
then
(
(phi . a1) . g2 in G &
x . 2
in A &
y . 2
in A &
x . 1
in G )
by Lm1, Lm3;
then
( the
multF of
G . (
(x . 1),
((phi . a1) . g2))
in G & the
multF of
A . (
(x . 2),
(y . 2))
in A )
by BINOP_1:17;
then reconsider z =
<*( the multF of G . ((x . 1),((phi . a1) . g2))),( the multF of A . ((x . 2),(y . 2)))*> as
Element of
product (Carrier <*G,A*>) by Lm2;
take
z
;
S1[x,y,z]
(
<*( the multF of G . ((x . 1),((phi . a1) . g2))),( the multF of A . ((x . 2),(y . 2)))*> = z &
a1 = x . 2 &
g2 = y . 1 &
<*( the multF of G . ((x . 1),((phi . a1) . g2))),( the multF of A . ((x . 2),(y . 2)))*> . 1
= the
multF of
G . (
(x . 1),
((phi . a1) . g2)) &
<*( the multF of G . ((x . 1),((phi . a1) . g2))),( the multF of A . ((x . 2),(y . 2)))*> . 2
= the
multF of
A . (
(x . 2),
(y . 2)) )
;
hence
S1[
x,
y,
z]
;
verum
end;
consider B being Function of [:(product (Carrier <*G,A*>)),(product (Carrier <*G,A*>)):],(product (Carrier <*G,A*>)) such that
A2:
for a, b being Element of product (Carrier <*G,A*>) holds S1[a,b,B . (a,b)]
from BINOP_1:sch 3(A1);
set M = multMagma(# (product (Carrier <*G,A*>)),B #);
reconsider M = multMagma(# (product (Carrier <*G,A*>)),B #) as non empty strict multMagma ;
take
M
; ( the carrier of M = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) )
thus
( the carrier of M = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) )
by A2; verum