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 -head ((Polish-operation (T,A,t)) . u) = t & 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 -head ((Polish-operation (T,A,t)) . u) = t & 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 -head ((Polish-operation (T,A,t)) . u) = t & 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 -head ((Polish-operation (T,A,t)) . u) = t & 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 -head ((Polish-operation (T,A,t)) . u) = 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 Def12;
hence ( T -head ((Polish-operation (T,A,t)) . u) = t & T -tail ((Polish-operation (T,A,t)) . u) = u ) ; :: thesis: verum