let b be bag of 1; :: thesis: rng (NBag1 | (Segm ((b . 0) + 1))) = { x where x is bag of 1 : x . 0 <= b . 0 }
A1: for o being object st o in rng (NBag1 | (Segm ((b . 0) + 1))) holds
o in { x where x is bag of 1 : x . 0 <= b . 0 }

proof

let o be object ; :: thesis: ( o in rng (NBag1 | (Segm ((b . 0) + 1))) implies o in { x where x is bag of 1 : x . 0 <= b . 0 } )
assume o in rng (NBag1 | (Segm ((b . 0) + 1))) ; :: thesis: o in { x where x is bag of 1 : x . 0 <= b . 0 }
then consider x being object such that
A2: ( x in dom (NBag1 | (Segm ((b . 0) + 1))) & o = (NBag1 | (Segm ((b . 0) + 1))) . x ) by FUNCT_1:def 3;
reconsider m1 = x as Element of NAT by A2;
m1 < (b . 0) + 1 by A2, NAT_1:44;
then A3: m1 <= b . 0 by NAT_1:13;
A4: (NBag1 | (Segm ((b . 0) + 1))) . x = NBag1 . x by A2, FUNCT_1:47
.= 1 --> m1 by Def1 ;
0 in 1 by CARD_1:49, TARSKI:def 1;
then (1 --> m1) . 0 = m1 by FUNCOP_1:7;
hence o in { x where x is bag of 1 : x . 0 <= b . 0 } by A3, A4, A2; :: thesis: verum

end;

for o being object st o in { x where x is bag of 1 : x . 0 <= b . 0 } holds
o in rng (NBag1 | (Segm ((b . 0) + 1)))

proof

let o be object ; :: thesis: ( o in { x where x is bag of 1 : x . 0 <= b . 0 } implies o in rng (NBag1 | (Segm ((b . 0) + 1))) )
assume o in { x where x is bag of 1 : x . 0 <= b . 0 } ; :: thesis: o in rng (NBag1 | (Segm ((b . 0) + 1)))
then consider x1 being bag of 1 such that
A5: ( o = x1 & x1 . 0 <= b . 0 ) ;
dom x1 = {0} by CARD_1:49, PARTFUN1:def 2;
then rng x1 = {(x1 . 0)} by FUNCT_1:4;
then A6: x1 = (dom x1) --> (x1 . 0) by FUNCOP_1:9
.= 1 --> (x1 . 0) by PARTFUN1:def 2 ;
reconsider m1 = x1 . 0 as Element of NAT ;
m1 < (b . 0) + 1 by A5, NAT_1:13;
then A7: m1 in dom (NBag1 | (Segm ((b . 0) + 1))) by NAT_1:44;
then (NBag1 | (Segm ((b . 0) + 1))) . m1 = NBag1 . m1 by FUNCT_1:47
.= 1 --> m1 by Def1 ;
hence o in rng (NBag1 | (Segm ((b . 0) + 1))) by A5, A6, A7, FUNCT_1:def 3; :: thesis: verum

end;

hence rng (NBag1 | (Segm ((b . 0) + 1))) = { x where x is bag of 1 : x . 0 <= b . 0 } by A1, TARSKI:2; :: thesis: verum