let K be non trivial Polish-language; :: thesis: for m, n being Nat
for a being object st a in K ^^ m & a in K ^^ n holds
m <= n
let m, n be Nat; :: thesis: for a being object st a in K ^^ m & a in K ^^ n holds
m <= n
let a be object ; :: thesis: ( a in K ^^ m & a in K ^^ n implies m <= n )
assume that
A1: a in K ^^ m and
A2: a in K ^^ n and
A3: m > n ; :: thesis: contradiction
consider k being Nat such that
A10: m = n + k by A3, NAT_1:10;
a in (K ^^ n) ^ (K ^^ k) by A1, A10, POLNOT_1:10;
then consider p, q being FinSequence such that
A12: a = p ^ q and
A13: p in K ^^ n and
A14: q in K ^^ k by POLNOT_1:def 2;
k = 0 by A2, A12, A13, A14, POLNOT_1:def 16;
hence contradiction by A3, A10; :: thesis: verum