let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I holds 1 -tuples_on [:{i}, the carrier of (G . i):] c= (FreeAtoms G) *
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I holds 1 -tuples_on [:{i}, the carrier of (G . i):] c= (FreeAtoms G) *
let G be Group-like multMagma-Family of I; :: thesis: 1 -tuples_on [:{i}, the carrier of (G . i):] c= (FreeAtoms G) *
set S = { [:{i}, the carrier of (G . i):] where i is Element of dom G : verum } ;

now :: thesis: for p being object st p in 1 -tuples_on [:{i}, the carrier of (G . i):] holds
p in (FreeAtoms G) *

let p be object ; :: thesis: ( p in 1 -tuples_on [:{i}, the carrier of (G . i):] implies p in (FreeAtoms G) * )
assume p in 1 -tuples_on [:{i}, the carrier of (G . i):] ; :: thesis: p in (FreeAtoms G) *
then consider z being set such that
A1: ( z in [:{i}, the carrier of (G . i):] & p = <*z*> ) by FINSEQ_2:135;
dom G = I by PARTFUN1:def 2;
then [:{i}, the carrier of (G . i):] in { [:{i}, the carrier of (G . i):] where i is Element of dom G : verum } ;
then z in union { [:{i}, the carrier of (G . i):] where i is Element of dom G : verum } by A1, TARSKI:def 4;
then z in FreeAtoms G by Th11;
then p is FinSequence of FreeAtoms G by A1, FINSEQ_1:74;
hence p in (FreeAtoms G) * by FINSEQ_1:def 11; :: thesis: verum

end;

hence 1 -tuples_on [:{i}, the carrier of (G . i):] c= (FreeAtoms G) * by TARSKI:def 3; :: thesis: verum