let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let i be Element of I; :: thesis: for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let x0 be set ; :: thesis: ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
defpred S₁[ set ] means ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);

A1: now :: thesis: ( x0 in ProjSet (F,i) implies ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )

assume x0 in ProjSet (F,i) ; :: thesis: ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
then consider g being Element of (F . i) such that
A2: x0 = (1_ (product F)) +* (i,g) by Def1;
reconsider x = x0 as Function by A2;
take x = x; :: thesis: ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
take g = g; :: thesis: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
thus x = x0 ; :: thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
thus ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by A2, Th1; :: thesis: verum

end;

now :: thesis: ( ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) implies x0 in ProjSet (F,i) )

assume A3: ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ; :: thesis: x0 in ProjSet (F,i)
thus x0 in ProjSet (F,i) :: thesis: verum

proof

consider x being Function, g being Element of (F . i) such that
A4: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by A3;
x = (1_ (product F)) +* (i,g) by Th1, A4;
hence x0 in ProjSet (F,i) by Def1, A4; :: thesis: verum

end;

end;

hence ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ) by A1; :: thesis: verum