let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let i be Element of I; :: thesis: for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let g be Element of (product F); :: thesis: ( g in ProjSet (F,i) implies g " in ProjSet (F,i) )
assume A1: g in ProjSet (F,i) ; :: thesis: g " in ProjSet (F,i)
consider z being Element of (F . i) such that
A2: g = (1_ (product F)) +* (i,z) by Def1, A1;
g " = (1_ (product F)) +* (i,(z ")) by Th4, A2;
hence g " in ProjSet (F,i) by Def1; :: thesis: verum