let IT1, IT2 be Element of F; :: thesis: ( ( ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) implies IT1 = IT2 ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) )
thus ( ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) implies IT1 = IT2 ) :: thesis: ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 )

proof

given p being Element of S such that A3: ( not a _|_ & not x _|_ ) ; :: thesis: ( ex q being Element of S st
( not a _|_ & not x _|_ & not IT1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) or ex q being Element of S st
( not a _|_ & not x _|_ & not IT2 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) or IT1 = IT2 )
consider r being Element of S such that
A4: ( not a _|_ & not x _|_ ) by A3;
assume that
A5: for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) and
A6: for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ; :: thesis: IT1 = IT2
IT1 = ((ProJ a,b,r) * (ProJ r,a,x)) * (ProJ x,r,y) by A5, A4;
hence IT1 = IT2 by A6, A4; :: thesis: verum

end;

thus ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) ; :: thesis: verum