let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for t being Element of T
for u being FinSequence holds
( t ^ u in Polish-WFF-set (T,A) iff u in (Polish-WFF-set (T,A)) ^^ (A . t) )
let A be Polish-arity-function of T; :: thesis: for t being Element of T
for u being FinSequence holds
( t ^ u in Polish-WFF-set (T,A) iff u in (Polish-WFF-set (T,A)) ^^ (A . t) )
let t be Element of T; :: thesis: for u being FinSequence holds
( t ^ u in Polish-WFF-set (T,A) iff u in (Polish-WFF-set (T,A)) ^^ (A . t) )
set W = Polish-WFF-set (T,A);
set n = A . t;
let u be FinSequence; :: thesis: ( t ^ u in Polish-WFF-set (T,A) iff u in (Polish-WFF-set (T,A)) ^^ (A . t) )
thus ( t ^ u in Polish-WFF-set (T,A) implies u in (Polish-WFF-set (T,A)) ^^ (A . t) ) :: thesis: ( u in (Polish-WFF-set (T,A)) ^^ (A . t) implies t ^ u in Polish-WFF-set (T,A) )

proof

assume t ^ u in Polish-WFF-set (T,A) ; :: thesis: u in (Polish-WFF-set (T,A)) ^^ (A . t)
then consider m being Nat, p, q being FinSequence such that
A11: p in T and
A12: m = A . p and
A13: t ^ u = (Polish-operation (T,A,m,p)) . q and
A14: q in (Polish-WFF-set (T,A)) ^^ m by POLNOT_1:38;
q in dom (Polish-operation (T,A,m,p)) by A14, FUNCT_2:def 1;
then A16: t ^ u = p ^ q by A11, A13, POLNOT_1:def 12;
t = T -head (p ^ q) by A16
.= p by A11, POLNOT_1:52 ;
hence u in (Polish-WFF-set (T,A)) ^^ (A . t) by A12, A14, A16, FINSEQ_1:33; :: thesis: verum

end;

thus ( u in (Polish-WFF-set (T,A)) ^^ (A . t) implies t ^ u in Polish-WFF-set (T,A) ) by Def6; :: thesis: verum