let n be non empty Ordinal; :: thesis: for x being Element of n holds degree (UnitBag x) = 1
let x be Element of n; :: thesis: degree (UnitBag x) = 1
set b = UnitBag x;
dom (UnitBag x) = n by PARTFUN1:def 2;
then A1: x in dom (UnitBag x) by SUBSET_1:def 1;
dom (EmptyBag n) = n by PARTFUN1:def 2;
then A2: x in dom (EmptyBag n) by SUBSET_1:def 1;
A3: (UnitBag x) * (canFS (support (UnitBag x))) = (UnitBag x) * (canFS {x}) by HILBASIS:8
.= (UnitBag x) * <*x*> by FINSEQ_1:94
.= <*((UnitBag x) . x)*> by A1, FINSEQ_2:34 ;
(UnitBag x) . x in rng (UnitBag x) by A1, FUNCT_1:3;
then reconsider f = (UnitBag x) * (canFS (support (UnitBag x))) as FinSequence of NAT by A3, FINSEQ_1:74;
degree (UnitBag x) = Sum f by UPROOTS:def 4
.= ((EmptyBag n) +* (x,1)) . x by A3, HILBASIS:def 2
.= 1 by A2, FUNCT_7:31 ;
hence degree (UnitBag x) = 1 ; :: thesis: verum