let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
ex fr being FinSequence of NAT st
( dom fr = dom a & ( for j being Nat st j in rng fr holds
SumBin (a,fr,{j}) <= 1 ) & ex k being Nat st rng fr = Seg k & card (rng f) = card (rng fr) )
let f be FinSequence of NAT ; :: thesis: ( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) implies ex fr being FinSequence of NAT st
( dom fr = dom a & ( for j being Nat st j in rng fr holds
SumBin (a,fr,{j}) <= 1 ) & ex k being Nat st rng fr = Seg k & card (rng f) = card (rng fr) ) )
assume that
DM00: dom f = dom a and
FS00: for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ; :: thesis: ex fr being FinSequence of NAT st
( dom fr = dom a & ( for j being Nat st j in rng fr holds
SumBin (a,fr,{j}) <= 1 ) & ex k being Nat st rng fr = Seg k & card (rng f) = card (rng fr) )
reconsider gix = Sgm0 (rng f) as XFinSequence of NAT ;
reconsider gi = XFS2FS gix as one-to-one Function ;
L040: rng gi = rng gix by AFINSQ_1:97
.= rng f by AFINSQ_2:def 4 ;
reconsider g = gi " as one-to-one Function ;
L400: dom g = rng f by FUNCT_1:33, L040;
then reconsider fr0 = g * f as FinSequence by FINSEQ_1:16;
L500: rng fr0 = rng g by L400, RELAT_1:28;
L520: rng fr0 = rng g by L400, RELAT_1:28
.= dom gi by FUNCT_1:33 ;
consider k0 being Nat such that
L530: dom gi = Seg k0 by FINSEQ_1:def 2;
reconsider fr0 = fr0 as FinSequence of NAT by L520, L530, FINSEQ_1:def 4;
take fr0 ; :: thesis: ( dom fr0 = dom a & ( for j being Nat st j in rng fr0 holds
SumBin (a,fr0,{j}) <= 1 ) & ex k being Nat st rng fr0 = Seg k & card (rng f) = card (rng fr0) )
thus dom fr0 = dom a by L400, RELAT_1:27, DM00; :: thesis: ( ( for j being Nat st j in rng fr0 holds
SumBin (a,fr0,{j}) <= 1 ) & ex k being Nat st rng fr0 = Seg k & card (rng f) = card (rng fr0) )
thus for j being Nat st j in rng fr0 holds
SumBin (a,fr0,{j}) <= 1 :: thesis: ( ex k being Nat st rng fr0 = Seg k & card (rng f) = card (rng fr0) )

proof

let j0 be Nat; :: thesis: ( j0 in rng fr0 implies SumBin (a,fr0,{j0}) <= 1 )
assume L710: j0 in rng fr0 ; :: thesis: SumBin (a,fr0,{j0}) <= 1
set j1 = (g ") . j0;
j0 in dom (g ") by L710, L500, FUNCT_1:33;
then L749: (g ") . j0 in rng (g ") by FUNCT_1:3;
then L750: (g ") . j0 in dom g by FUNCT_1:33;
L760: (g ") . j0 in rng f by L749, FUNCT_1:43, L040;
L761: j0 = g . ((g ") . j0) by L710, L500, FUNCT_1:32;
for x being object holds
( x in {((g ") . j0)} iff ( x in dom g & g . x in {j0} ) )

proof

let x be object ; :: thesis: ( x in {((g ") . j0)} iff ( x in dom g & g . x in {j0} ) )

hereby :: thesis: ( x in dom g & g . x in {j0} implies x in {((g ") . j0)} )

assume L762: x in {((g ") . j0)} ; :: thesis: ( x in dom g & g . x in {j0} )
hence x in dom g by TARSKI:def 1, L750; :: thesis: g . x in {j0}
g . x = j0 by L762, TARSKI:def 1, L761;
hence g . x in {j0} by TARSKI:def 1; :: thesis: verum

end;

assume that
L764: x in dom g and
L765: g . x in {j0} ; :: thesis: x in {((g ") . j0)}
g . x = j0 by L765, TARSKI:def 1;
then x = (g ") . j0 by L764, FUNCT_1:32;
hence x in {((g ") . j0)} by TARSKI:def 1; :: thesis: verum

end;

then g " {j0} = {((g ") . j0)} by FUNCT_1:def 7;
then SumBin (a,fr0,{j0}) = SumBin (a,f,{((g ") . j0)}) by RELAT_1:146;
hence SumBin (a,fr0,{j0}) <= 1 by L760, FS00; :: thesis: verum

end;

thus ex k being Nat st rng fr0 = Seg k by L520, L530; :: thesis: card (rng f) = card (rng fr0)
card (dom gi) = card (rng (gi ")) by FUNCT_1:33
.= card (rng fr0) by L400, RELAT_1:28 ;
hence card (rng f) = card (rng fr0) by CARD_1:70, L040; :: thesis: verum