let p be Prime; :: thesis: for g being positive-yielding bag of Seg p st g = p |-> p holds
g = g * (canFS (support g))
let f be positive-yielding bag of Seg p; :: thesis: ( f = p |-> p implies f = f * (canFS (support f)) )
assume A0: f = p |-> p ; :: thesis: f = f * (canFS (support f))
Y1: dom f = Seg p by A0;
then yy: support f = Seg p by Thds;
set g = f * (canFS (Seg p));
R5: rng (canFS (Seg p)) = Seg p by FUNCT_2:def 3;
R3: dom (canFS (Seg p)) = Seg p by domcanFS;
R4: dom (f * (canFS (Seg p))) = dom (canFS (Seg p)) by RELAT_1:27, R5, Y1
.= Seg p by domcanFS ;
then GG: dom (f * (canFS (Seg p))) = dom (p |-> p) ;
for x being object st x in dom (f * (canFS (Seg p))) holds
(f * (canFS (Seg p))) . x = (p |-> p) . x
proof
let x be object ; :: thesis: ( x in dom (f * (canFS (Seg p))) implies (f * (canFS (Seg p))) . x = (p |-> p) . x )
assume Z2: x in dom (f * (canFS (Seg p))) ; :: thesis: (f * (canFS (Seg p))) . x = (p |-> p) . x
hence (f * (canFS (Seg p))) . x = f . ((canFS (Seg p)) . x) by FUNCT_1:12
.= p by Z2, FUNCOP_1:7, A0, R5, R3, R4, FUNCT_1:3
.= (p |-> p) . x by FUNCOP_1:7, Z2, R4 ;
:: thesis: verum
end;
hence f = f * (canFS (support f)) by A0, yy, FUNCT_1:2, GG; :: thesis: verum