let n be Nat; :: thesis:
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
set B = BagOrder n;
set B1 = BagOrder (n + 1);
set P = p extended_by_0 ;
A1: n -' 0 = n by NAT_D:40;
A2: ( BagOrder n linearly_orders Support p & BagOrder (n + 1) linearly_orders Support (p extended_by_0) ) by POLYNOM2:18;
deffunc H₁( bag of n) -> Element of Bags (n + 1) = $1 bag_extend 0;
A3: for x being Element of Bags n holds H₁(x) in Bags (n + 1) ;
consider f being Function of (Bags n),(Bags (n + 1)) such that
A4: for x being Element of Bags n holds f . x = H₁(x) from FUNCT_2:sch 8(A3);
set F = f | (Support p);
A5: dom (f | (Support p)) = Support p by FUNCT_2:def 1;
set Sp = SgmX ((BagOrder n),(Support p));
set SP = SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)));
A6: rng (f | (Support p)) c= Support (p extended_by_0)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (f | (Support p)) ; :: thesis:
then consider x being object such that
A7: ( x in dom (f | (Support p)) & (f | (Support p)) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags n by A7, A5;
A8: f . x = (f | (Support p)) . x by A7, FUNCT_1:47;
f . x = H₁(x) by A4;
hence y in Support (p extended_by_0) by A7, A8, Th8; :: thesis:

end;

Support (p extended_by_0) c= rng (f | (Support p))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: y in Support (p extended_by_0) ; :: thesis:
then reconsider b = y as bag of n + 1 ;
set C = (0,n) -cut b;
A10: b . n = 0 by A9, Th7;
then A11: (0,n) -cut b in Support p by A9, Th9;
then reconsider C = (0,n) -cut b as Element of Bags n ;
( H₁(C) = f . C & f . C = (f | (Support p)) . C ) by A11, A4, FUNCT_1:49;
then A12: H₁(C) in rng (f | (Support p)) by A11, A5, FUNCT_1:def 3;
n -' 0 = n by NAT_D:40;
hence y in rng (f | (Support p)) by A12, A10, Th4; :: thesis:

end;

then A13: Support (p extended_by_0) = rng (f | (Support p)) by A6, XBOOLE_0:def 10;
f | (Support p) is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume A14: ( x1 in dom (f | (Support p)) & x2 in dom (f | (Support p)) & (f | (Support p)) . x1 = (f | (Support p)) . x2 ) ; :: thesis:
reconsider x1 = x1, x2 = x2 as Element of Bags n by A14, A5;
A15: ( f . x1 = (f | (Support p)) . x1 & f . x2 = (f | (Support p)) . x2 ) by A14, FUNCT_1:47;
( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A4;
then ( H₁(x1) = H₁(x2) & x1 = H₁(x1) | n ) by HILBASIS:def 1, A15, A14;
hence x1 = x2 by HILBASIS:def 1; :: thesis:

end;

then A16: ( len (SgmX ((BagOrder n),(Support p))) = card (Support p) & card (Support p) = card (Support (p extended_by_0)) & card (Support (p extended_by_0)) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) ) by CARD_1:5, POLYNOM2:18, PRE_POLY:11, A5, A13, WELLORD2:def 4;
hence len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) ; :: thesis:
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len (SgmX ((BagOrder n),(Support p))) implies for i being Nat st 1 <= i & i <= $1 holds
(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 );
A17: ( rng (SgmX ((BagOrder n),(Support p))) = Support p & rng (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) = Support (p extended_by_0) ) by A2, PRE_POLY:def 2;
A18: S₁[ 0 ] ;
A19: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

per cases by NAT_1:14;

suppose A30: k = 0 ; :: thesis:

A31: i = 1 by A30, A22, XXREAL_0:1;
A32: ((SgmX ((BagOrder n),(Support p))) /. 1) bag_extend 0 in Support (p extended_by_0) by Th8, A30, A29, A28, A17;
for y being Element of Bags (n + 1) st y in Support (p extended_by_0) holds
[(((SgmX ((BagOrder n),(Support p))) /. 1) bag_extend 0),y] in BagOrder (n + 1)

proof

let y be Element of Bags (n + 1); :: thesis:
set Y = (0,n) -cut y;
assume A33: y in Support (p extended_by_0) ; :: thesis:
then y . n = 0 by Th7;
then (0,n) -cut y in Support p by A33, Th9;
then consider w being object such that
A34: ( w in dom (SgmX ((BagOrder n),(Support p))) & (SgmX ((BagOrder n),(Support p))) . w = (0,n) -cut y ) by FUNCT_1:def 3, A17;
y . n = 0 by Th7, A33;
then A35: y = ((0,n) -cut y) bag_extend 0 by Th4;
reconsider w = w as Nat by A34;
A36: (SgmX ((BagOrder n),(Support p))) . w = (SgmX ((BagOrder n),(Support p))) /. w by A34, PARTFUN1:def 6;
A37: 1 <= w by A34, FINSEQ_3:25;

per cases by A37, XXREAL_0:1;

suppose w = 1 ; :: thesis:

hence [(((SgmX ((BagOrder n),(Support p))) /. 1) bag_extend 0),y] in BagOrder (n + 1) by PRE_POLY:def 14, A35, A1, A34, A36; :: thesis:

end;

suppose w > 1 ; :: thesis:

end;

hence (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 by A31, A32, POLYNOM2:18, PRE_POLY:20; :: thesis:

end;

suppose A39: k >= 1 ; :: thesis:

proof

assume A51: not ((SgmX ((BagOrder n),(Support p))) /. (k + 1)) bag_extend 0 in rng ((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) | (k + 1)) ; :: thesis:
e > k + 1

proof

assume e <= k + 1 ; :: thesis:
then e in Seg (k + 1) by A47;
hence contradiction by A51, A48, A46, PARTFUN2:18; :: thesis:

end;

then A52: (SgmX ((BagOrder n),(Support p))) /. f < (SgmX ((BagOrder n),(Support p))) /. (k + 1) by A43, A44, Th14, A46, A27, A45, A48, Th16;
A53: ( k in dom (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & k in dom (SgmX ((BagOrder n),(Support p))) ) by A23, A39, A16, FINSEQ_3:25;
A54: k < k + 1 by NAT_1:13;
A55: (SgmX ((BagOrder n),(Support p))) /. k < (SgmX ((BagOrder n),(Support p))) /. f by A43, A44, Th14, A49, A45, Th16, A27, A53, A54;
then A56: k <> f ;

per cases ;

suppose k <= f ; :: thesis:

then k < f by A56, XXREAL_0:1;
then ( k + 1 <= f & k + 1 <> f ) by A52, NAT_1:13;
then k + 1 < f by XXREAL_0:1;
hence contradiction by A52, A43, A27, Th16; :: thesis:

end;

suppose k > f ; :: thesis:

hence contradiction by A55, A43, A53, Th16; :: thesis:

end;

A57: rng ((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) | (k + 1)) = (rng ((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) | k)) \/ (rng <*((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) . (k + 1))*>) by A26, FINSEQ_1:31
.= (rng ((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) | k)) \/ {((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) . (k + 1))} by FINSEQ_1:38 ;
A58: ((SgmX ((BagOrder n),(Support p))) /. (k + 1)) bag_extend 0 = (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) . (k + 1)

proof

end;

per cases by A22, XXREAL_0:1;

suppose i < k + 1 ; :: thesis:

then i <= k by NAT_1:13;
hence (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 by A22, A20, A21, NAT_1:13, A39; :: thesis:

end;

suppose i = k + 1 ; :: thesis:

hence (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 by A58, A27, PARTFUN1:def 6; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A18, A19);
hence for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds
(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ; :: thesis: