let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being Group-Family of J
for x being Function st a is one-to-one & x in sum F holds
x * a in sum (F * a)
let a be Function of I,J; :: thesis: for F being Group-Family of J
for x being Function st a is one-to-one & x in sum F holds
x * a in sum (F * a)
let F be Group-Family of J; :: thesis: for x being Function st a is one-to-one & x in sum F holds
x * a in sum (F * a)
let x be Function; :: thesis: ( a is one-to-one & x in sum F implies x * a in sum (F * a) )
assume A1: a is one-to-one ; :: thesis: ( not x in sum F or x * a in sum (F * a) )
assume A2: x in sum F ; :: thesis: x * a in sum (F * a)
then x in product F by GROUP_2:40;
then reconsider x = x as Element of (product F) ;
reconsider Fa = F * a as Group-Family of I ;
x * a in product (F * a) by Th1;
then reconsider xa = x * a as Element of (product (F * a)) ;
A3: dom a = I by FUNCT_2:def 1;
A4: a .: (support (xa,Fa)) c= support (x,F) by Th7;
a .: (support (xa,Fa)), support (xa,Fa) are_equipotent by A1, A3, CARD_1:33;
then support (xa,Fa) is finite by A2, A4, CARD_1:38;
hence x * a in sum (F * a) by GROUP_19:8; :: thesis: verum