let G be commutative Group; :: thesis: for I0, I being non empty finite set
for q being Element of I
for x being b₂ -defined the carrier of G -valued total Function
for x0 being b₁ -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}

proof

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;

Product x = (Product x0) * (Product y) by A2, A1, Th8;
hence Product x = (Product x0) * k by Th9; :: thesis: verum