let I be non empty set ; :: thesis: for F being Group-Family of I
for G being strict Subgroup of product F
for S being Subgroup-Family of F st ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) holds
for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G
let F be Group-Family of I; :: thesis: for G being strict Subgroup of product F
for S being Subgroup-Family of F st ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) holds
for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G
let G be strict Subgroup of product F; :: thesis: for S being Subgroup-Family of F st ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) holds
for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G
let S be Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) implies for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G )
assume for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ; :: thesis: for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G
let f be Homomorphism-Family of G,S; :: thesis: ( ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) implies product f = id the carrier of G )
assume A2: for i being Element of I holds f . i = (proj (F,i)) * (incl G) ; :: thesis: product f = id the carrier of G
A3: for g being Element of G
for i being Element of I holds ((proj (F,i)) * (incl G)) . g = ((proj (F,i)) * (product f)) . g

proof

let g be Element of G; :: thesis: for i being Element of I holds ((proj (F,i)) * (incl G)) . g = ((proj (F,i)) * (product f)) . g
let i be Element of I; :: thesis: ((proj (F,i)) * (incl G)) . g = ((proj (F,i)) * (product f)) . g
(product f) . g in product S ;
then B2: (product f) . g in product F by GROUP_2:40;
B3: ((product f) . g) . i = (proj (F,i)) . ((product f) . g) by B2, Def13
.= ((proj (F,i)) * (product f)) . g by FUNCT_2:15 ;
((proj (F,i)) * (incl G)) . g = (f . i) . g by A2
.= ((product f) . g) . i by Def14 ;
hence ((proj (F,i)) * (incl G)) . g = ((proj (F,i)) * (product f)) . g by B3; :: thesis: verum

end;

A4: for g being Element of (product F) st g in G holds
(product f) . g = g

proof

let g be Element of (product F); :: thesis: ( g in G implies (product f) . g = g )
assume B1: g in G ; :: thesis: (product f) . g = g
(product f) . g in product F

proof

(product f) . g in product S by B1, FUNCT_2:5;
hence (product f) . g in product F by GROUP_2:40; :: thesis: verum

end;

then reconsider foo = (product f) . g as Element of (product F) ;
B2: for i being Element of I holds ((proj (F,i)) * (incl G)) . g = g . i

proof

let i be Element of I; :: thesis: ((proj (F,i)) * (incl G)) . g = g . i
((proj (F,i)) * (incl G)) . g = (proj (F,i)) . ((incl G) . g) by B1, FUNCT_2:15
.= (proj (F,i)) . ((id the carrier of G) . g) by Def9
.= (proj (F,i)) . g by B1, FUNCT_1:18
.= g . i by Def13 ;
hence ((proj (F,i)) * (incl G)) . g = g . i ; :: thesis: verum

end;

B3: ( dom g = I & dom foo = I ) by GROUP_19:3;
for i being Element of I holds foo . i = g . i

proof

let i be Element of I; :: thesis: foo . i = g . i
(proj (F,i)) . foo = ((proj (F,i)) * (product f)) . g by B1, FUNCT_2:15
.= ((proj (F,i)) * (incl G)) . g by B1, A3
.= g . i by B2 ;
hence foo . i = g . i by Def13; :: thesis: verum

end;

then foo = g by B3;
hence (product f) . g = g ; :: thesis: verum

end;

A6: dom (product f) = the carrier of G by FUNCT_2:def 1;
for x being object st x in the carrier of G holds
(product f) . x = x

proof

let x be object ; :: thesis: ( x in the carrier of G implies (product f) . x = x )
assume x in the carrier of G ; :: thesis: (product f) . x = x
then B1: x in G ;
then x in product F by GROUP_2:40;
hence (product f) . x = x by B1, A4; :: thesis: verum

end;

hence product f = id the carrier of G by A6, FUNCT_1:17; :: thesis: verum