let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for A being finite Subset of V

for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let A be finite Subset of V; :: thesis: for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let E be Enumeration of A; :: thesis: for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let v be Element of V; :: thesis: E + ((card A) |-> v) is Enumeration of v + A

A1: rng E = A by Def1;

then A2: len E = card A by FINSEQ_4:62;

then reconsider e = E, cAv = (card A) |-> v as Element of (card A) -tuples_on the carrier of V by FINSEQ_2:92;

A3: len (e + cAv) = card A by CARD_1:def 7;

then A4: dom (e + cAv) = Seg (card A) by FINSEQ_1:def 3;

A5: dom e = Seg (card A) by A2, FINSEQ_1:def 3;

A6: rng (e + cAv) c= v + A

card A = card (v + A) by RLAFFIN1:7;

then e + cAv is one-to-one by A3, A14, FINSEQ_4:62;

hence E + ((card A) |-> v) is Enumeration of v + A by A14, Def1; :: thesis: verum

for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let A be finite Subset of V; :: thesis: for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let E be Enumeration of A; :: thesis: for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

let v be Element of V; :: thesis: E + ((card A) |-> v) is Enumeration of v + A

A1: rng E = A by Def1;

then A2: len E = card A by FINSEQ_4:62;

then reconsider e = E, cAv = (card A) |-> v as Element of (card A) -tuples_on the carrier of V by FINSEQ_2:92;

A3: len (e + cAv) = card A by CARD_1:def 7;

then A4: dom (e + cAv) = Seg (card A) by FINSEQ_1:def 3;

A5: dom e = Seg (card A) by A2, FINSEQ_1:def 3;

A6: rng (e + cAv) c= v + A

proof

v + A c= rng (e + cAv)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (e + cAv) or y in v + A )

assume y in rng (e + cAv) ; :: thesis: y in v + A

then consider x being object such that

A7: x in dom (e + cAv) and

A8: (e + cAv) . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A7;

A9: e . x in rng e by A5, A4, A7, FUNCT_1:def 3;

then reconsider Ex = e . x as Element of V ;

cAv . x = v by A4, A7, FINSEQ_2:57;

then y = Ex + v by A7, A8, FVSUM_1:17;

then y = v + Ex by RLVECT_1:def 2;

then y in { (v + w) where w is Element of V : w in A } by A1, A9;

hence y in v + A by RUSUB_4:def 8; :: thesis: verum

end;assume y in rng (e + cAv) ; :: thesis: y in v + A

then consider x being object such that

A7: x in dom (e + cAv) and

A8: (e + cAv) . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A7;

A9: e . x in rng e by A5, A4, A7, FUNCT_1:def 3;

then reconsider Ex = e . x as Element of V ;

cAv . x = v by A4, A7, FINSEQ_2:57;

then y = Ex + v by A7, A8, FVSUM_1:17;

then y = v + Ex by RLVECT_1:def 2;

then y in { (v + w) where w is Element of V : w in A } by A1, A9;

hence y in v + A by RUSUB_4:def 8; :: thesis: verum

proof

then A14:
v + A = rng (e + cAv)
by A6;
let vA be object ; :: according to TARSKI:def 3 :: thesis: ( not vA in v + A or vA in rng (e + cAv) )

assume vA in v + A ; :: thesis: vA in rng (e + cAv)

then vA in { (v + a) where a is Element of V : a in A } by RUSUB_4:def 8;

then consider a being Element of V such that

A10: vA = v + a and

A11: a in A ;

consider x being object such that

A12: x in dom E and

A13: E . x = a by A1, A11, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A12;

cAv . x = v by A5, A12, FINSEQ_2:57;

then (e + cAv) . x = a + v by A5, A4, A12, A13, FVSUM_1:17

.= vA by A10, RLVECT_1:def 2 ;

hence vA in rng (e + cAv) by A5, A4, A12, FUNCT_1:def 3; :: thesis: verum

end;assume vA in v + A ; :: thesis: vA in rng (e + cAv)

then vA in { (v + a) where a is Element of V : a in A } by RUSUB_4:def 8;

then consider a being Element of V such that

A10: vA = v + a and

A11: a in A ;

consider x being object such that

A12: x in dom E and

A13: E . x = a by A1, A11, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A12;

cAv . x = v by A5, A12, FINSEQ_2:57;

then (e + cAv) . x = a + v by A5, A4, A12, A13, FVSUM_1:17

.= vA by A10, RLVECT_1:def 2 ;

hence vA in rng (e + cAv) by A5, A4, A12, FUNCT_1:def 3; :: thesis: verum

card A = card (v + A) by RLAFFIN1:7;

then e + cAv is one-to-one by A3, A14, FINSEQ_4:62;

hence E + ((card A) |-> v) is Enumeration of v + A by A14, Def1; :: thesis: verum