let U1, U2 be Universal_Algebra; :: thesis: ( UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) implies for G being GeneratorSet of U1 holds G is GeneratorSet of U2 )
assume A1: UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) ; :: thesis: for G being GeneratorSet of U1 holds G is GeneratorSet of U2
let G be GeneratorSet of U1; :: thesis: G is GeneratorSet of U2
reconsider G2 = G as Subset of U2 by A1;
G2 is GeneratorSet of U2
proof
let A be Subset of U2; :: according to FREEALG:def 4 :: thesis: ( not A is opers_closed or not G2 c= A or A = the carrier of U2 )
reconsider B = A as Subset of U1 by A1;
assume A is opers_closed ; :: thesis: ( not G2 c= A or A = the carrier of U2 )
hence ( not G2 c= A or A = the carrier of U2 ) by A1, Th40, FREEALG:def 4; :: thesis: verum
end;
hence G is GeneratorSet of U2 ; :: thesis: verum