let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
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 (Support p) 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 (Support p) 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 (Support p) 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 (Support p) holds
Low p,T,(i + 1) = Red (Low p,T,i),T
let i be Element of NAT ; :: thesis: ( i < card (Support p) implies Low p,T,(i + 1) = Red (Low p,T,i),T )
assume A1: i < card (Support p) ; :: thesis: Low p,T,(i + 1) = Red (Low p,T,i),T
then A2: i + 1 <= card (Support p) by NAT_1:13;
set l = Low p,T,i;
set l1 = Low p,T,(i + 1);
set r = Red (Low p,T,i),T;
A3: 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 ;
A4: (Support (Low p,T,i)) \ (Support (Low p,T,(i + 1))) = {(HT (Low p,T,i),T)} by A1, Th42;
A5: Support (Low p,T,i) c= Support p by A1, Th26;
A6: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
A7: Support (Low p,T,(i + 1)) = Lower_Support p,T,(i + 1) by A2, Lm3;
A8: Support (Low p,T,(i + 1)) = Lower_Support p,T,(i + 1) by A2, Lm3;
A9: card (Support (Low p,T,i)) = (card (Support p)) - i by A1, A6, Th24;
A10: card (Support (Low p,T,(i + 1))) = (card (Support p)) - (i + 1) by A2, A8, Th24;

now

assume A11: {(HT (Low p,T,i),T)} /\ (Support (Low p,T,(i + 1))) <> {} ; :: thesis: contradiction
consider u being Element of {(HT (Low p,T,i),T)} /\ (Support (Low p,T,(i + 1)));
A12: ( u in {(HT (Low p,T,i),T)} & u in Support (Low p,T,(i + 1)) ) by A11, XBOOLE_0:def 4;
then u = HT (Low p,T,i),T by TARSKI:def 1;
then A13: HT (Low p,T,i),T <= HT (Low p,T,(i + 1)),T,T by A12, TERMORD:def 6;
A14: HT (Low p,T,(i + 1)),T in Support (Low p,T,(i + 1)) by A12, TERMORD:def 6;

now

let u' be set ; :: thesis: ( u' in Support (Low p,T,i) implies u' in Support (Low p,T,(i + 1)) )
assume A15: u' in Support (Low p,T,i) ; :: thesis: u' in Support (Low p,T,(i + 1))
then reconsider u = u' as Element of Bags n ;
u <= HT (Low p,T,i),T,T by A15, TERMORD:def 6;
then u <= HT (Low p,T,(i + 1)),T,T by A13, TERMORD:8;
hence u' in Support (Low p,T,(i + 1)) by A2, A5, A7, A14, A15, Th24; :: thesis: verum

end;

then Support (Low p,T,i) c= Support (Low p,T,(i + 1)) by TARSKI:def 3;
then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A9, A10, NAT_1:44;
then - i <= - (i + 1) by XREAL_1:8;
then i + 1 <= i by XREAL_1:26;
then (i + 1) - i <= i - i by XREAL_1:11;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum

end;

then A16: Support (Low p,T,(i + 1)) misses {(HT (Low p,T,i),T)} by XBOOLE_0:def 7;
A17: Support (Low p,T,(i + 1)) c= Support (Low p,T,i) by A1, Th41;
Support (Low p,T,i) = (Support (Low p,T,(i + 1))) \/ {(HT (Low p,T,i),T)} by A1, A4, Th41, XBOOLE_1:45;
then A18: 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 A16, XBOOLE_1:83 ;

now

let x be set ; :: 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

per cases ( b in Support (Low p,T,(i + 1)) or not b in Support (Low p,T,(i + 1)) ) ;

case A19: 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 A4, XBOOLE_0:def 5;
then A20: b <> HT (Low p,T,i),T by TARSKI:def 1;
thus (Low p,T,(i + 1)) . b = p . b by A2, A19, Th31
.= (Low p,T,i) . b by A1, A17, A19, Th31
.= (Red (Low p,T,i),T) . b by A17, A19, A20, TERMORD:40 ; :: thesis: verum

end;

case A21: 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 9
.= (Red (Low p,T,i),T) . b by A18, A21, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

hence (Low p,T,(i + 1)) . x = (Red (Low p,T,i),T) . x ; :: thesis: verum

end;

hence Low p,T,(i + 1) = Red (Low p,T,i),T by A3, FUNCT_1:9; :: thesis: verum