let T be Polish-language; for A being Polish-arity-function of T
for t being Element of T
for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds
T -tail ((Polish-operation (T,A,t)) . u) = u
let A be Polish-arity-function of T; for t being Element of T
for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds
T -tail ((Polish-operation (T,A,t)) . u) = u
let t be Element of T; for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds
T -tail ((Polish-operation (T,A,t)) . u) = u
let u be FinSequence; ( u in (Polish-WFF-set (T,A)) ^^ (A . t) implies T -tail ((Polish-operation (T,A,t)) . u) = u )
set W = Polish-WFF-set (T,A);
set f = Polish-operation (T,A,t);
assume
u in (Polish-WFF-set (T,A)) ^^ (A . t)
; T -tail ((Polish-operation (T,A,t)) . u) = u
then
u in dom (Polish-operation (T,A,t))
by FUNCT_2:def 1;
then
(Polish-operation (T,A,t)) . u = t ^ u
by Def13;
hence
T -tail ((Polish-operation (T,A,t)) . u) = u
by Th17; verum