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) )

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

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

thus
ex k being Nat st rng fr0 = Seg k
by L520, L530; :: thesis: card (rng f) = card (rng fr0)
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} ) )

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;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

then
g " {j0} = {((g ") . j0)}
by FUNCT_1:def 7;
let x be object ; :: thesis: ( x in {((g ") . j0)} iff ( x in dom g & g . x in {j0} ) )

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;hereby :: thesis: ( x in dom g & g . x in {j0} implies x in {((g ") . j0)} )

assume that 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;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

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

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

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