let I be non empty set ; for i being Element of I
for F being Group-Family of I holds Image (proj (F,i)) = multMagma(# the carrier of (F . i), the multF of (F . i) #)
let i be Element of I; for F being Group-Family of I holds Image (proj (F,i)) = multMagma(# the carrier of (F . i), the multF of (F . i) #)
let F be Group-Family of I; Image (proj (F,i)) = multMagma(# the carrier of (F . i), the multF of (F . i) #)
for g being object st g in the carrier of (F . i) holds
g in the carrier of (Image (proj (F,i)))
proof
let g be
object ;
( g in the carrier of (F . i) implies g in the carrier of (Image (proj (F,i))) )
assume
g in the
carrier of
(F . i)
;
g in the carrier of (Image (proj (F,i)))
then reconsider x =
g as
Element of
(F . i) ;
ex
h being
Element of
(product F) st
x = (proj (F,i)) . h
proof
dom (1_ (product F)) = I
by GROUP_19:3;
then B1:
((1_ (product F)) +* (i,x)) . i = x
by FUNCT_7:31;
(1_ (product F)) +* (
i,
x)
in ProjSet (
F,
i)
by GROUP_12:def 1;
then reconsider h =
(1_ (product F)) +* (
i,
x) as
Element of
(product F) ;
take
h
;
x = (proj (F,i)) . h
(proj (F,i)) . ((1_ (product F)) +* (i,x)) =
(proj (F,i)) . h
.=
x
by B1, Def13
;
hence
x = (proj (F,i)) . h
;
verum
end;
then
x in Image (proj (F,i))
by GROUP_6:45;
hence
g in the
carrier of
(Image (proj (F,i)))
;
verum
end;
hence
Image (proj (F,i)) = multMagma(# the carrier of (F . i), the multF of (F . i) #)
by GROUP_2:61, TARSKI:def 3; verum