let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for a being object st T is trivial & a in T holds
A . a = 0
let A be Polish-arity-function of T; :: thesis: for a being object st T is trivial & a in T holds
A . a = 0
let a be object ; :: thesis: ( T is trivial & a in T implies A . a = 0 )
assume A1: ( T is trivial & a in T ) ; :: thesis: A . a = 0
consider b being object such that
A3: ( b in T & A . b = 0 ) by POLNOT_1:def 18;
thus A . a = 0 by A1, A3, ZFMISC_1:def 10; :: thesis: verum