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

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