let U1 be Universal_Algebra; :: thesis: id the carrier of U1 is_homomorphism
thus U1,U1 are_similar ; :: according to ALG_1:def 1 :: thesis: for n being Nat st n in dom the charact of U1 holds
for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
let n be Nat; :: thesis: ( n in dom the charact of U1 implies for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume n in dom the charact of U1 ; :: thesis: for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
let o1, o2 be operation of U1; :: thesis: ( o1 = the charact of U1 . n & o2 = the charact of U1 . n implies for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume A1: ( o1 = the charact of U1 . n & o2 = the charact of U1 . n ) ; :: thesis: for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
set f = id the carrier of U1;
let x be FinSequence of U1; :: thesis: ( x in dom o1 implies (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume x in dom o1 ; :: thesis: (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
then o1 . x in rng o1 by FUNCT_1:def 3;
then reconsider u = o1 . x as Element of U1 ;
(id the carrier of U1) . u = u ;
hence (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) by A1, Th3; :: thesis: verum