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);

L: now

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
R1: x0 = (1_ (product F)) +* (i,g) by defPrj;
reconsider x = x0 as Function by R1;
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 R1, LMPX1; :: thesis: verum

end;

now

assume R1: 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
Q1: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by R1;
x = (1_ (product F)) +* (i,g) by LMPX1, Q1;
hence x0 in ProjSet (F,i) by defPrj, Q1; :: 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 L; :: thesis: verum