let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism & h1 = h " holds
h1 is_homomorphism
let h be Function of U1,U2; :: thesis: for h1 being Function of U2,U1 st h is_isomorphism & h1 = h " holds
h1 is_homomorphism
let h1 be Function of U2,U1; :: thesis: ( h is_isomorphism & h1 = h " implies h1 is_homomorphism )
assume that
A1: h is_isomorphism and
A2: h1 = h " ; :: thesis: h1 is_homomorphism
A3: h is one-to-one by A1, Th7;
A4: h is_homomorphism by A1, Th7;
then A5: U1,U2 are_similar ;
then A6: signature U1 = signature U2 ;
A7: ( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def 3, UNIALG_1:def 4;
A8: dom (signature U2) = Seg (len (signature U2)) by FINSEQ_1:def 3;
A9: ( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) ) by FINSEQ_1:def 3, UNIALG_1:def 4;
A10: rng h = the carrier of U2 by A1, Th7;

now :: thesis: for n being Nat st n in dom the charact of U2 holds
for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)

let n be Nat; :: thesis: ( n in dom the charact of U2 implies for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )
assume A11: n in dom the charact of U2 ; :: thesis: for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let o2 be operation of U2; :: thesis: for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let o1 be operation of U1; :: thesis: ( o2 = the charact of U2 . n & o1 = the charact of U1 . n implies for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )
assume A12: ( o2 = the charact of U2 . n & o1 = the charact of U1 . n ) ; :: thesis: for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let x be FinSequence of U2; :: thesis: ( x in dom o2 implies h1 . (o2 . x) = o1 . (h1 * x) )
defpred S₁[ set , set ] means h . $2 = x . $1;
A13: dom x = Seg (len x) by FINSEQ_1:def 3;
A14: for m being Nat st m in Seg (len x) holds
ex a being Element of U1 st S₁[m,a]

proof

let m be Nat; :: thesis: ( m in Seg (len x) implies ex a being Element of U1 st S₁[m,a] )
assume m in Seg (len x) ; :: thesis: ex a being Element of U1 st S₁[m,a]
then m in dom x by FINSEQ_1:def 3;
then x . m in the carrier of U2 by FINSEQ_2:11;
then consider a being object such that
A15: a in dom h and
A16: h . a = x . m by A10, FUNCT_1:def 3;
reconsider a = a as Element of U1 by A15;
take a ; :: thesis: S₁[m,a]
thus S₁[m,a] by A16; :: thesis: verum

end;

consider p being FinSequence of U1 such that
A17: ( dom p = Seg (len x) & ( for m being Nat st m in Seg (len x) holds
S₁[m,p . m] ) ) from FINSEQ_1:sch 5(A14);
A18: dom (h * p) = dom p by FINSEQ_3:120;

now :: thesis: for n being Nat st n in dom x holds
x . n = (h * p) . n

let n be Nat; :: thesis: ( n in dom x implies x . n = (h * p) . n )
assume A19: n in dom x ; :: thesis: x . n = (h * p) . n
hence x . n = h . (p . n) by A17, A13
.= (h * p) . n by A17, A13, A18, A19, FINSEQ_3:120 ;
:: thesis: verum

end;

then A20: x = h * p by A17, A13, A18;
A21: len p = len x by A17, FINSEQ_1:def 3;
assume x in dom o2 ; :: thesis: h1 . (o2 . x) = o1 . (h1 * x)
then x in (arity o2) -tuples_on the carrier of U2 by MARGREL1:22;
then x in { s where s is Element of the carrier of U2 * : len s = arity o2 } by FINSEQ_2:def 4;
then A22: ex s being Element of the carrier of U2 * st
( x = s & len s = arity o2 ) ;
A23: h1 * h = id (dom h) by A2, A3, FUNCT_1:39
.= id the carrier of U1 by FUNCT_2:def 1 ;
then A24: h1 * x = (id the carrier of U1) * p by A20, Th4
.= p by Th3 ;
reconsider p = p as Element of the carrier of U1 * by FINSEQ_1:def 11;
( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A6, A8, A9, A11, A12, UNIALG_1:def 4;
then p in { w where w is Element of the carrier of U1 * : len w = arity o1 } by A6, A22, A21;
then p in (arity o1) -tuples_on the carrier of U1 by FINSEQ_2:def 4;
then A25: p in dom o1 by MARGREL1:22;
then A26: h1 . (o2 . x) = h1 . (h . (o1 . p)) by A4, A6, A7, A9, A11, A12, A20;
A27: o1 . p in the carrier of U1 by A25, PARTFUN1:4;
then o1 . p in dom h by FUNCT_2:def 1;
hence h1 . (o2 . x) = (id the carrier of U1) . (o1 . p) by A23, A26, FUNCT_1:13
.= o1 . (h1 * x) by A24, A27, FUNCT_1:17 ;
:: thesis: verum

end;

hence h1 is_homomorphism by A5; :: thesis: verum