let k, n be Nat; :: thesis: for b1, b2 being bag of n holds
( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )
let b1, b2 be bag of n; :: thesis: ( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )
set B1 = b1 bag_extend k;
set B2 = b2 bag_extend k;
A1: ( (b1 bag_extend k) | n = b1 & (b2 bag_extend k) | n = b2 & (b1 bag_extend k) . n = k & k = (b2 bag_extend k) . n ) by HILBASIS:def 1;
A2: ( dom b2 = n & n = dom b1 ) by PARTFUN1:def 2;
thus ( b1 < b2 implies b1 bag_extend k < b2 bag_extend k ) :: thesis: ( b1 bag_extend k < b2 bag_extend k implies b1 < b2 )

proof

assume b1 < b2 ; :: thesis: b1 bag_extend k < b2 bag_extend k
then consider o being Ordinal such that
A3: b1 . o < b2 . o and
A4: for l being Ordinal st l in o holds
b1 . l = b2 . l by PRE_POLY:def 9;
A5: o in dom b2 by A3, FUNCT_1:def 2;
then A6: ( (b2 bag_extend k) . o = b2 . o & (b1 bag_extend k) . o = b1 . o ) by A1, FUNCT_1:47, A2;
for l being Ordinal st l in o holds
(b1 bag_extend k) . l = (b2 bag_extend k) . l

proof

let l be Ordinal; :: thesis: ( l in o implies (b1 bag_extend k) . l = (b2 bag_extend k) . l )
assume A7: l in o ; :: thesis: (b1 bag_extend k) . l = (b2 bag_extend k) . l
then ( (b2 bag_extend k) . l = b2 . l & (b1 bag_extend k) . l = b1 . l ) by A1, FUNCT_1:47, A2, A5, ORDINAL1:10;
hence (b1 bag_extend k) . l = (b2 bag_extend k) . l by A7, A4; :: thesis: verum

end;

hence b1 bag_extend k < b2 bag_extend k by A3, A6, PRE_POLY:def 9; :: thesis: verum

end;

assume b1 bag_extend k < b2 bag_extend k ; :: thesis: b1 < b2
then consider o being Ordinal such that
A8: (b1 bag_extend k) . o < (b2 bag_extend k) . o and
A9: for l being Ordinal st l in o holds
(b1 bag_extend k) . l = (b2 bag_extend k) . l by PRE_POLY:def 9;
o in dom (b2 bag_extend k) by A8, FUNCT_1:def 2;
then o in Segm (n + 1) ;
then o in (Segm n) \/ {n} by AFINSQ_1:2;
then A10: ( o in n or o = n ) by ZFMISC_1:136;
then A11: ( (b2 bag_extend k) . o = b2 . o & (b1 bag_extend k) . o = b1 . o ) by A1, A8, FUNCT_1:47, A2;
for l being Ordinal st l in o holds
b1 . l = b2 . l

proof

let l be Ordinal; :: thesis: ( l in o implies b1 . l = b2 . l )
assume A12: l in o ; :: thesis: b1 . l = b2 . l
then ( (b2 bag_extend k) . l = b2 . l & (b1 bag_extend k) . l = b1 . l ) by A2, A10, A1, FUNCT_1:47, ORDINAL1:10;
hence b1 . l = b2 . l by A12, A9; :: thesis: verum

end;

hence b1 < b2 by A8, A11, PRE_POLY:def 9; :: thesis: verum