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

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

hence
G is GeneratorSet of U2
; :: thesis: verum
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;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