reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
deffunc H1( Element of X) -> set = (b . $1) |^ n;
defpred S1[ object , object ] means ex a being Element of X st
( a = $1 & $2 = H1(a) );
A1: n1 >= 1 by NAT_1:53;
A2: for e being object st e in X holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in X implies ex u being object st S1[e,u] )
assume e in X ; :: thesis: ex u being object st S1[e,u]
then reconsider f = e as Element of X ;
take H1(f) ; :: thesis: S1[e,H1(f)]
take f ; :: thesis: ( f = e & H1(f) = H1(f) )
thus ( f = e & H1(f) = H1(f) ) ; :: thesis: verum
end;
consider f being Function such that
A3: dom f = X and
A4: for x being object st x in X holds
S1[x,f . x] from CLASSES1:sch 1(A2);
 reconsider f = f as ManySortedSet of X by A3, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: ( support f = support b & ( for i being object holds f . i = (b . i) |^ n ) )
A5: dom b = X by PARTFUN1:def 2;
now :: thesis: for x being object holds
( ( x in support f implies x in support b ) & ( x in support b implies x in support f ) )
let x be object ; :: thesis: ( ( x in support f implies x in support b ) & ( x in support b implies x in support f ) )
reconsider xx = x as set by TARSKI:1;
hereby :: thesis: ( x in support b implies x in support f )
assume A6: x in support f ; :: thesis: x in support b
assume not x in support b ; :: thesis: contradiction
then b . x = 0 by PRE_POLY:def 7;
then A7: (b . xx) |^ n = 0 by A1, NEWTON:11;
support f c= X by A3, PRE_POLY:37;
then S1[x,f . x] by A4, A6;
hence contradiction by A6, A7, PRE_POLY:def 7; :: thesis: verum
end;
A8: now :: thesis: f . x = (b . xx) |^ n1
per cases ( x in X or not x in X ) ;
suppose x in X ; :: thesis: f . x = (b . xx) |^ n1
then S1[x,f . x] by A4;
hence f . x = (b . xx) |^ n1 ; :: thesis: verum
end;
suppose A9: not x in X ; :: thesis: f . x = (b . xx) |^ n1
hence f . x = 0 by A3, FUNCT_1:def 2
.= 0 |^ n1 by A1, NEWTON:11
.= (b . xx) |^ n1 by A5, A9, FUNCT_1:def 2 ;
:: thesis: verum
end;
end;
end;
assume x in support b ; :: thesis: x in support f
then b . x <> 0 by PRE_POLY:def 7;
then f . x <> 0 by A8, CARD_4:3;
hence x in support f by PRE_POLY:def 7; :: thesis: verum
end;
hence support f = support b by TARSKI:2; :: thesis: for i being object holds f . i = (b . i) |^ n
let i be object ; :: thesis: f . i = (b . i) |^ n
per cases ( i in X or not i in X ) ;
suppose i in X ; :: thesis: f . i = (b . i) |^ n
then S1[i,f . i] by A4;
hence f . i = (b . i) |^ n ; :: thesis: verum
end;
suppose A10: not i in X ; :: thesis: f . i = (b . i) |^ n
hence f . i = 0 by A3, FUNCT_1:def 2
.= 0 |^ n by A1, NEWTON:11
.= (b . i) |^ n by A5, A10, FUNCT_1:def 2 ;
:: thesis: verum
end;
end;