let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; 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; 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; for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
let v be Element of V; 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
v + A c= rng (e + cAv)
proof
let vA be
object ;
TARSKI:def 3 ( not vA in v + A or vA in rng (e + cAv) )
assume
vA in v + A
;
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;
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 A3, A14, FINSEQ_4:62;
hence
E + ((card A) |-> v) is Enumeration of v + A
by A14, Def1; verum