let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I
for g being Element of (product F) holds (proj (F,i)) . g = (proj ((Carrier F),i)) . g
let i be Element of I; :: thesis: for F being Group-Family of I
for g being Element of (product F) holds (proj (F,i)) . g = (proj ((Carrier F),i)) . g
let F be Group-Family of I; :: thesis: for g being Element of (product F) holds (proj (F,i)) . g = (proj ((Carrier F),i)) . g
let g be Element of (product F); :: thesis: (proj (F,i)) . g = (proj ((Carrier F),i)) . g
set X = product (Carrier F);
set f = proj ((Carrier F),i);
A1: dom (proj ((Carrier F),i)) = product (Carrier F) by CARD_3:def 16;
g in product F ;
then g in dom (proj ((Carrier F),i)) by A1, GROUP_7:def 2;
then (proj ((Carrier F),i)) . g = g . i by CARD_3:def 16;
hence (proj (F,i)) . g = (proj ((Carrier F),i)) . g by Def13; :: thesis: verum