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 ;
A6: rng (e + cAv) c= v + A
proof
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 ;
then reconsider Ex = e . x as Element of V ;
cAv . x = v by ;
then y = Ex + v by ;
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;
v + A c= rng (e + cAv)
proof
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 ;
reconsider x = x as Element of NAT by A12;
cAv . x = v by ;
then (e + cAv) . x = a + v by
.= vA by ;
hence vA in rng (e + cAv) by ; :: thesis: verum
end;
then A14: v + A = rng (e + cAv) by A6;
card A = card (v + A) by RLAFFIN1:7;
then e + cAv is one-to-one by ;
hence E + ((card A) |-> v) is Enumeration of v + A by ; :: thesis: verum