reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Element of X) -> set = (b . $1) |^ n;
defpred S₁[ object , object ] means ex a being Element of X st
( a = $1 & $2 = H₁(a) );
A1: n1 >= 1 by NAT_1:53;
A2: for e being object st e in X holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in X implies ex u being object st S₁[e,u] )
assume e in X ; :: thesis: ex u being object st S₁[e,u]
then reconsider f = e as Element of X ;
take H₁(f) ; :: thesis: S₁[e,H₁(f)]
take f ; :: thesis: ( f = e & H₁(f) = H₁(f) )
thus ( f = e & H₁(f) = H₁(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
S₁[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 S₁[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 S₁[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 S₁[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;