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_{1}[ set ] means ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);

( 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

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

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

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

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

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

end;( 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

( 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