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 bijective holds
( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )
let a be Function of I,J; :: thesis: for F being Group-Family of J
for x being Function st a is bijective holds
( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )
let F be Group-Family of J; :: thesis: for x being Function st a is bijective holds
( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )
let x be Function; :: thesis: ( a is bijective implies ( x in sum F iff ( x * a in sum (F * a) & dom x = J ) ) )
assume A1: a is bijective ; :: thesis: ( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )

hereby :: thesis: ( x * a in sum (F * a) & dom x = J implies x in sum F )

assume A2: x in sum F ; :: thesis: ( x * a in sum (F * a) & dom x = J )
then x in product F by GROUP_2:40;
hence ( x * a in sum (F * a) & dom x = J ) by A1, A2, Th9, GROUP_19:3; :: thesis: verum

end;

assume A3: ( x * a in sum (F * a) & dom x = J ) ; :: thesis: x in sum F
A4: ( rng a = J & a is one-to-one ) by A1, FUNCT_2:def 3;
then reconsider b = a " as Function of J,I by FUNCT_2:25;
A5: ( a * b = id J & b * a = id I ) by A4, FUNCT_2:29;
A6: dom F = J by PARTFUN1:def 2;
(x * a) * b in sum ((F * a) * b) by A3, A1, Th9;
then x * (a * b) in sum ((F * a) * b) by RELAT_1:36;
then x * (id J) in sum (F * (id J)) by A5, RELAT_1:36;
then x in sum (F * (id J)) by A3, RELAT_1:52;
hence x in sum F by A6, RELAT_1:52; :: thesis: verum