let G be Group; :: thesis: for I, J being non empty set
for F being DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is DirectSumComponents of G,I
let I, J be non empty set ; :: thesis: for F being DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is DirectSumComponents of G,I
let F be DirectSumComponents of G,J; :: thesis: for a being Function of I,J st a is bijective holds
F * a is DirectSumComponents of G,I
let a be Function of I,J; :: thesis: ( a is bijective implies F * a is DirectSumComponents of G,I )
assume A1: a is bijective ; :: thesis: F * a is DirectSumComponents of G,I
consider h1 being Homomorphism of (sum F),G such that
A2: h1 is bijective by GROUP_19:def 8;
reconsider h2 = trans_sum (F,a) as Homomorphism of (sum F),(sum (F * a)) by A1, TT;
A3: h2 is bijective by A1, Th12;
then reconsider h3 = h2 " as Homomorphism of (sum (F * a)),(sum F) by GROUP_6:62;
reconsider h = h1 * h3 as Homomorphism of (sum (F * a)),G ;
h3 is bijective by A3, GROUP_6:63;
then h is bijective by A2, GROUP_6:64;
hence F * a is DirectSumComponents of G,I by GROUP_19:def 8; :: thesis: verum