let G be commutative Group; :: thesis: for I0, I being non empty finite set

for q being Element of I

for x being b_{2} -defined the carrier of G -valued total Function

for x0 being b_{1} -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let I0, I be non empty finite set ; :: thesis: for q being Element of I

for x being I -defined the carrier of G -valued total Function

for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let q be Element of I; :: thesis: for x being I -defined the carrier of G -valued total Function

for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let x be I -defined the carrier of G -valued total Function; :: thesis: for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let x0 be I0 -defined the carrier of G -valued total Function; :: thesis: for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let k be Element of G; :: thesis: ( not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) implies Product x = (Product x0) * k )

assume A1: ( not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) ) ; :: thesis: Product x = (Product x0) * k

reconsider y = q .--> k as {q} -defined the carrier of G -valued total Function ;

A2: I0 misses {q}

hence Product x = (Product x0) * k by Th9; :: thesis: verum

for q being Element of I

for x being b

for x0 being b

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let I0, I be non empty finite set ; :: thesis: for q being Element of I

for x being I -defined the carrier of G -valued total Function

for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let q be Element of I; :: thesis: for x being I -defined the carrier of G -valued total Function

for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let x be I -defined the carrier of G -valued total Function; :: thesis: for x0 being I0 -defined the carrier of G -valued total Function

for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let x0 be I0 -defined the carrier of G -valued total Function; :: thesis: for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds

Product x = (Product x0) * k

let k be Element of G; :: thesis: ( not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) implies Product x = (Product x0) * k )

assume A1: ( not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) ) ; :: thesis: Product x = (Product x0) * k

reconsider y = q .--> k as {q} -defined the carrier of G -valued total Function ;

A2: I0 misses {q}

proof

Product x = (Product x0) * (Product y)
by A2, A1, Th8;
assume
I0 meets {q}
; :: thesis: contradiction

then consider x being object such that

A3: ( x in I0 & x in {q} ) by XBOOLE_0:3;

thus contradiction by A3, A1, TARSKI:def 1; :: thesis: verum

end;then consider x being object such that

A3: ( x in I0 & x in {q} ) by XBOOLE_0:3;

thus contradiction by A3, A1, TARSKI:def 1; :: thesis: verum

hence Product x = (Product x0) * k by Th9; :: thesis: verum