defpred S₁[ object ] means ex t being Element of T ex u being Element of T * st
( $1 = t ^ u & u in U ^^ (A . t) );
set X = Polish-expression-layer (T,A,U);
let Y be Subset of (T *); :: thesis: ( Y = Polish-expression-layer (T,A,U) iff for a being object holds
( a in Y iff ex t being Element of T ex u being Element of T * st
( a = t ^ u & u in U ^^ (A . t) ) ) )
A1: for a being object holds
( a in Polish-expression-layer (T,A,U) iff S₁[a] )

proof

let a be object ; :: thesis: ( a in Polish-expression-layer (T,A,U) iff S₁[a] )
thus ( a in Polish-expression-layer (T,A,U) implies S₁[a] ) :: thesis: ( S₁[a] implies a in Polish-expression-layer (T,A,U) )

proof

assume a in Polish-expression-layer (T,A,U) ; :: thesis: S₁[a]
then consider t, q being FinSequence, n being Nat such that
A3: a = t ^ q and
A4: t in T and
A5: n = A . t and
A6: q in U ^^ n by Def6;
reconsider t1 = t as Element of T by A4;
U ^^ n c= T * by Th14;
then reconsider q1 = q as Element of T * by A6;
take t1 ; :: thesis: ex u being Element of T * st
( a = t1 ^ u & u in U ^^ (A . t1) )
take q1 ; :: thesis: ( a = t1 ^ q1 & q1 in U ^^ (A . t1) )
thus ( a = t1 ^ q1 & q1 in U ^^ (A . t1) ) by A3, A5, A6; :: thesis: verum

end;

assume S₁[a] ; :: thesis: a in Polish-expression-layer (T,A,U)
then consider t being Element of T, u being Element of T * such that
A10: a = t ^ u and
A11: u in U ^^ (A . t) ;
set n = A . t;
T c= T * by Th9;
then t in T * ;
then a in T * by A10, Th12;
hence a in Polish-expression-layer (T,A,U) by A10, A11, Def6; :: thesis: verum

end;

hence ( Polish-expression-layer (T,A,U) = Y implies for a being object holds
( a in Y iff S₁[a] ) ) ; :: thesis: ( ( for a being object holds
( a in Y iff ex t being Element of T ex u being Element of T * st
( a = t ^ u & u in U ^^ (A . t) ) ) ) implies Y = Polish-expression-layer (T,A,U) )
assume A20: for a being object holds
( a in Y iff S₁[a] ) ; :: thesis: Y = Polish-expression-layer (T,A,U)
thus Polish-expression-layer (T,A,U) = Y from XBOOLE_0:sch 2(A1, A20); :: thesis: verum