let T be Polish-language; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum