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