let M, N be non empty multMagma ; :: thesis: for f being Function of M,N
for X being Subset of M st f is multiplicative holds
f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))
let f be Function of M,N; :: thesis: for X being Subset of M st f is multiplicative holds
f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))
let X be Subset of M; :: thesis: ( f is multiplicative implies f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X)) )
assume A1: f is multiplicative ; :: thesis: f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))
set X9 = the_submagma_generated_by X;
set A = f .: the carrier of (the_submagma_generated_by X);
the carrier of (the_submagma_generated_by X) is stable Subset of M by Th8;
then reconsider A = f .: the carrier of (the_submagma_generated_by X) as stable Subset of N by A1, Th11;
set Y9 = the_submagma_generated_by (f .: X);
set B = f " the carrier of (the_submagma_generated_by (f .: X));
the carrier of (the_submagma_generated_by (f .: X)) is stable Subset of N by Th8;
then reconsider B = f " the carrier of (the_submagma_generated_by (f .: X)) as stable Subset of M by A1, Th12;
A2: ( f .: X c= the carrier of (the_submagma_generated_by (f .: X)) & ( for N1 being strict multSubmagma of N st f .: X c= the carrier of N1 holds
the_submagma_generated_by (f .: X) is multSubmagma of N1 ) ) by Def12;
reconsider N1 = multMagma(# A,(the_mult_induced_by A) #) as strict multSubmagma of N by Def9;
X c= the carrier of (the_submagma_generated_by X) by Def12;
then the_submagma_generated_by (f .: X) is multSubmagma of N1 by A2, RELAT_1:123;
then A3: the carrier of (the_submagma_generated_by (f .: X)) c= A by Def9;
A4: ( X c= the carrier of (the_submagma_generated_by X) & ( for M1 being strict multSubmagma of M st X c= the carrier of M1 holds
the_submagma_generated_by X is multSubmagma of M1 ) ) by Def12;
reconsider M1 = multMagma(# B,(the_mult_induced_by B) #) as strict multSubmagma of M by Def9;
A5: f .: (f " the carrier of (the_submagma_generated_by (f .: X))) c= the carrier of (the_submagma_generated_by (f .: X)) by FUNCT_1:75;
f .: X c= the carrier of (the_submagma_generated_by (f .: X)) by Def12;
then A6: f " (f .: X) c= f " the carrier of (the_submagma_generated_by (f .: X)) by RELAT_1:143;
X c= the carrier of M ;
then X c= dom f by FUNCT_2:def 1;
then X c= f " (f .: X) by FUNCT_1:76;
then the_submagma_generated_by X is multSubmagma of M1 by A4, A6, XBOOLE_1:1;
then the carrier of (the_submagma_generated_by X) c= B by Def9;
then A c= f .: (f " the carrier of (the_submagma_generated_by (f .: X))) by RELAT_1:123;
then A c= the carrier of (the_submagma_generated_by (f .: X)) by A5;
hence f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X)) by A3, XBOOLE_0:def 10; :: thesis: verum