let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t being Element of L
for a being object st a in dom (Polish-operation (L,E,t)) holds
ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t )
let E be Polish-arity-function of L; :: thesis: for t being Element of L
for a being object st a in dom (Polish-operation (L,E,t)) holds
ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t )
let t be Element of L; :: thesis: for a being object st a in dom (Polish-operation (L,E,t)) holds
ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t )
let a be object ; :: thesis: ( a in dom (Polish-operation (L,E,t)) implies ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t ) )
assume A1: a in dom (Polish-operation (L,E,t)) ; :: thesis: ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t )
then a in (Polish-WFF-set (L,E)) ^^ (E . t) by FUNCT_2:def 1;
then reconsider q = a as FinSequence ;
take t ^ q ; :: thesis: ( t ^ q = (Polish-operation (L,E,t)) . a & L -head (t ^ q) = t )
thus (Polish-operation (L,E,t)) . a = t ^ q by A1, Def12; :: thesis: L -head (t ^ q) = t
thus L -head (t ^ q) = t ; :: thesis: verum