let n be Nat; :: thesis: for b being bag of n holds SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))
let b be bag of n; :: thesis: SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))
set S1 = SgmX ((RelIncl n),(support b));
set B = b bag_extend 0;
set S2 = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)));
A1: RelIncl n linearly_orders support b by PRE_POLY:82;
A2: RelIncl (n + 1) linearly_orders support (b bag_extend 0) by PRE_POLY:82;
A3: ( rng (SgmX ((RelIncl n),(support b))) = support b & rng (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) = support (b bag_extend 0) ) by A1, A2, PRE_POLY:def 2;
A4: support b = support (b bag_extend 0) by Th11;
then reconsider s2 = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))) as FinSequence of n by A3, FINSEQ_1:def 4;
reconsider R1 = RelIncl (n + 1) as Order of (n + 1) ;
for n1, m1 being Nat st n1 in dom s2 & m1 in dom s2 & n1 < m1 holds
( s2 /. n1 <> s2 /. m1 & [(s2 /. n1),(s2 /. m1)] in RelIncl n )

proof

let n1, m1 be Nat; :: thesis: ( n1 in dom s2 & m1 in dom s2 & n1 < m1 implies ( s2 /. n1 <> s2 /. m1 & [(s2 /. n1),(s2 /. m1)] in RelIncl n ) )
assume A5: ( n1 in dom s2 & m1 in dom s2 & n1 < m1 ) ; :: thesis: ( s2 /. n1 <> s2 /. m1 & [(s2 /. n1),(s2 /. m1)] in RelIncl n )
[((SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. n1),((SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. m1)] in RelIncl (n + 1) by A5, A2, PRE_POLY:def 2;
then A6: (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. n1 c= (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. m1 by WELLORD2:def 1;
A7: ( (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. n1 = (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) . n1 & (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) . n1 = s2 /. n1 ) by A5, PARTFUN1:def 6;
A8: ( (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) /. m1 = (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) . m1 & (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) . m1 = s2 /. m1 ) by A5, PARTFUN1:def 6;
( s2 . n1 in rng (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) & s2 . m1 in rng (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) ) by A5, FUNCT_1:def 3;
hence ( s2 /. n1 <> s2 /. m1 & [(s2 /. n1),(s2 /. m1)] in RelIncl n ) by A5, A2, PRE_POLY:def 2, A6, A7, A8, A3, A4, WELLORD2:def 1; :: thesis: verum

end;

hence SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))) by A3, A4, A1, PRE_POLY:def 2; :: thesis: verum