[:(1 *),1:] c= [:(1 *),1:] ;
then reconsider DER = [:(1 *),1:] as non empty Relation of (1 *),1 ;
reconsider EM = typestr(# 1,op2,op2,op2,DER #) as non empty typestr ;
take EM ; :: thesis: EM is SynTypes_Calculus-like
A1: for x being type of EM
for X being FinSequence of EM holds X ==>. x

proof

let x be type of EM; :: thesis: for X being FinSequence of EM holds X ==>. x
let X be FinSequence of EM; :: thesis: X ==>. x
[X,x] in [:(1 *),1:] ;
hence X ==>. x by Def18; :: thesis: verum

end;

hence for x being type of EM holds <*x*> ==>. x ; :: according to PRELAMB:def 18 :: thesis: ( ( for T being FinSequence of EM
for x, y being type of EM st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of EM
for x, y being type of EM st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds
(X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y being type of EM st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) )
thus ( ( for T being FinSequence of EM
for x, y being type of EM st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of EM
for x, y being type of EM st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds
(X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y being type of EM st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) ) by A1; :: thesis: verum