let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for p being Polynomial of n,L
for i being Element of NAT st i < card () holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card () holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for i being Element of NAT st i < card () holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card () holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let i be Element of NAT ; :: thesis: ( i < card () implies Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) )
set l = Low (p,T,i);
set l1 = Low (p,T,(i + 1));
set r = Red ((Low (p,T,i)),T);
assume A1: i < card () ; :: thesis: Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)
then A2: Support (Low (p,T,i)) c= Support p by Th26;
Support (Low (p,T,i)) = Lower_Support (p,T,i) by ;
then A3: card (Support (Low (p,T,i))) = (card ()) - i by ;
A4: Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) by ;
A5: i + 1 <= card () by ;
then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;
then A6: card (Support (Low (p,T,(i + 1)))) = (card ()) - (i + 1) by ;
A7: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by ;
now :: thesis: not {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) <> {}
set u = the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1))));
assume A8: {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) <> {} ; :: thesis: contradiction
then the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in {(HT ((Low (p,T,i)),T))} by XBOOLE_0:def 4;
then A9: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) = HT ((Low (p,T,i)),T) by TARSKI:def 1;
A10: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in Support (Low (p,T,(i + 1))) by ;
now :: thesis: for u9 being object st u9 in Support (Low (p,T,i)) holds
u9 in Support (Low (p,T,(i + 1)))
let u9 be object ; :: thesis: ( u9 in Support (Low (p,T,i)) implies u9 in Support (Low (p,T,(i + 1))) )
assume A11: u9 in Support (Low (p,T,i)) ; :: thesis: u9 in Support (Low (p,T,(i + 1)))
then reconsider u = u9 as Element of Bags n ;
u <= HT ((Low (p,T,i)),T),T by ;
hence u9 in Support (Low (p,T,(i + 1))) by A5, A2, A7, A10, A9, A11, Th24; :: thesis: verum
end;
then Support (Low (p,T,i)) c= Support (Low (p,T,(i + 1))) ;
then (card ()) + (- i) <= (card ()) + (- (i + 1)) by ;
then - i <= - (i + 1) by XREAL_1:6;
then i + 1 <= i by XREAL_1:24;
then (i + 1) - i <= i - i by XREAL_1:9;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum
end;
then A12: Support (Low (p,T,(i + 1))) misses {(HT ((Low (p,T,i)),T))} by XBOOLE_0:def 7;
A13: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} by ;
then Support (Low (p,T,i)) = (Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))} by ;
then A14: Support (Red ((Low (p,T,i)),T)) = ((Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))}) \ {(HT ((Low (p,T,i)),T))} by TERMORD:36
.= (Support (Low (p,T,(i + 1)))) \ {(HT ((Low (p,T,i)),T))} by XBOOLE_1:40
.= Support (Low (p,T,(i + 1))) by ;
A15: now :: thesis: for x being object st x in dom (Low (p,T,(i + 1))) holds
(Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x
let x be object ; :: thesis: ( x in dom (Low (p,T,(i + 1))) implies (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x )
assume x in dom (Low (p,T,(i + 1))) ; :: thesis: (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x
then reconsider b = x as Element of Bags n ;
now :: thesis: ( ( b in Support (Low (p,T,(i + 1))) & (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b ) or ( not b in Support (Low (p,T,(i + 1))) & (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b ) )
per cases ( b in Support (Low (p,T,(i + 1))) or not b in Support (Low (p,T,(i + 1))) ) ;
case A16: b in Support (Low (p,T,(i + 1))) ; :: thesis: (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b
then not b in {(HT ((Low (p,T,i)),T))} by ;
then A17: b <> HT ((Low (p,T,i)),T) by TARSKI:def 1;
thus (Low (p,T,(i + 1))) . b = p . b by
.= (Low (p,T,i)) . b by A1, A4, A16, Th31
.= (Red ((Low (p,T,i)),T)) . b by ; :: thesis: verum
end;
case A18: not b in Support (Low (p,T,(i + 1))) ; :: thesis: (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b
hence (Low (p,T,(i + 1))) . b = 0. L by POLYNOM1:def 4
.= (Red ((Low (p,T,i)),T)) . b by ;
:: thesis: verum
end;
end;
end;
hence (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x ; :: thesis: verum
end;
dom (Low (p,T,(i + 1))) = Bags n by FUNCT_2:def 1
.= dom (Red ((Low (p,T,i)),T)) by FUNCT_2:def 1 ;
hence Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) by ; :: thesis: verum