let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I holds rng (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (G . i):]
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I holds rng (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (G . i):]
let G be Group-like multMagma-Family of I; :: thesis: rng (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (G . i):]
set C = the carrier of (G . i);
A1: dom (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = the carrier of (G . i) by Th53;

now :: thesis: for p being object holds
( ( p in 1 -tuples_on [:{i}, the carrier of (G . i):] implies p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) ) & ( p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) implies p in 1 -tuples_on [:{i}, the carrier of (G . i):] ) )

let p be object ; :: thesis: ( ( p in 1 -tuples_on [:{i}, the carrier of (G . i):] implies p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) ) & ( p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) implies p in 1 -tuples_on [:{i}, the carrier of (G . i):] ) )

hereby :: thesis: ( p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) implies p in 1 -tuples_on [:{i}, the carrier of (G . i):] )

assume p in 1 -tuples_on [:{i}, the carrier of (G . i):] ; :: thesis: p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>))
then p is Tuple of 1,[:{i}, the carrier of (G . i):] by FINSEQ_2:131;
then consider z being Element of [:{i}, the carrier of (G . i):] such that
A2: p = <*z*> by FINSEQ_2:97;
consider x, g being object such that
A3: ( x in {i} & g in the carrier of (G . i) & z = [x,g] ) by ZFMISC_1:def 2;
reconsider g = g as Element of (G . i) by A3;
x = i by A3, TARSKI:def 1;
then (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g = p by A2, A3, Th54;
hence p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) by A1, FUNCT_1:3; :: thesis: verum

end;

assume p in rng (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) ; :: thesis: p in 1 -tuples_on [:{i}, the carrier of (G . i):]
then consider g being object such that
A4: g in dom (curry' (uncurry <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>)) and
A5: (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g = p by FUNCT_1:def 3;
reconsider g = g as Element of (G . i) by A1, A4;
A6: p = <*[i,g]*> by A5, Th54;
( i in {i} & g in the carrier of (G . i) ) by TARSKI:def 1;
then [i,g] in [:{i}, the carrier of (G . i):] by ZFMISC_1:def 2;
hence p in 1 -tuples_on [:{i}, the carrier of (G . i):] by A6, FINSEQ_2:98; :: thesis: verum

end;

hence rng (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (G . i):] by TARSKI:2; :: thesis: verum