set A = Polish-arity V;
reconsider t = t as Element of dom (Polish-arity V) by FUNCT_2:def 1;
take Polish-unOp ((Polish-arity V),Q,t) ; :: thesis: for p being FinSequence st p in Q holds
(Polish-unOp ((Polish-arity V),Q,t)) . p = t ^ p
thus for p being FinSequence st p in Q holds
(Polish-unOp ((Polish-arity V),Q,t)) . p = t ^ p by A1, Def15; :: thesis: verum