let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar holds
for o being OperSymbol of (MSSign U1)
for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1)
for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y )
assume A1: U1,U2 are_similar ; :: thesis: for o being OperSymbol of (MSSign U1)
for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y
reconsider f1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
let o be OperSymbol of (MSSign U1); :: thesis: for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y
A2: the carrier' of (MSSign U2) = dom (signature U2) by MSUALG_1:def 8;
MSSign U1 = MSSign U2 by A1, Th10;
then o in dom (signature U2) by A2;
then A3: o in dom (signature U1) by A1;
then o in dom f1 by FUNCT_2:def 1;
then A4: ((*--> 0) * (signature U1)) . o = (*--> 0) . ((signature U1) . o) by FUNCT_1:12;
let y be Element of Args (o,(MSAlg U1)); :: thesis: (MSAlg h) # y = h * y
set f = MSAlg h;
A5: the carrier of (MSSign U1) = {0} by MSUALG_1:def 8;
set X = dom (h * y);
A6: dom h = the carrier of U1 by FUNCT_2:def 1;
A7: y is FinSequence of the carrier of U1 by Th14;
then rng y c= the carrier of U1 by FINSEQ_1:def 4;
then reconsider p = h * y as FinSequence by A7, A6, FINSEQ_1:16;
A8: dom (h * y) = dom y by A7, FINSEQ_3:120;
the Arity of (MSSign U1) = f1 by MSUALG_1:def 8;
then A9: the_arity_of o = ((*--> 0) * (signature U1)) . o by MSUALG_1:def 1;
(signature U1) . o in rng (signature U1) by A3, FUNCT_1:def 3;
then consider n being Element of NAT such that
A10: n = (signature U1) . o ;
A11: 0 in {0} by TARSKI:def 1;

A12: now :: thesis: for m being Nat st m in dom y holds
(MSAlg h) . ((the_arity_of o) /. m) = h

0 is Element of {0} by TARSKI:def 1;
then n |-> 0 is FinSequence of {0} by FINSEQ_2:63;
then reconsider l = n |-> 0 as Element of the carrier of (MSSign U1) * by A5, FINSEQ_1:def 11;
let m be Nat; :: thesis: ( m in dom y implies (MSAlg h) . ((the_arity_of o) /. m) = h )
A13: ( (the_arity_of o) /. m = l /. m & dom (n |-> 0) = Seg n ) by A9, A4, A10, FINSEQ_2:def 6;
assume m in dom y ; :: thesis: (MSAlg h) . ((the_arity_of o) /. m) = h
then m in dom (the_arity_of o) by MSUALG_3:6;
then A14: m in dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def 6;
then l /. m = l . m by PARTFUN1:def 6;
then (the_arity_of o) /. m = 0 by A14, A13, FUNCOP_1:7;
hence (MSAlg h) . ((the_arity_of o) /. m) = (0 .--> h) . 0 by A1, Def3, Th10
.= h by A11, FUNCOP_1:7 ;
:: thesis: verum

end;

A15: now :: thesis: for m being Nat st m in dom y holds
((MSAlg h) # y) . m = p . m

let m be Nat; :: thesis: ( m in dom y implies ((MSAlg h) # y) . m = p . m )
assume A16: m in dom y ; :: thesis: ((MSAlg h) # y) . m = p . m
then A17: m in dom (h * y) by A7, FINSEQ_3:120;
((MSAlg h) # y) . m = ((MSAlg h) . ((the_arity_of o) /. m)) . (y . m) by A16, MSUALG_3:def 6;
hence ((MSAlg h) # y) . m = h . (y . m) by A12, A16
.= p . m by A7, A17, FINSEQ_3:120 ;
:: thesis: verum

end;

dom ((MSAlg h) # y) = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def 6
.= Seg n ;
then A18: (MSAlg h) # y is FinSequence by FINSEQ_1:def 2;
A19: dom y = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def 6
.= Seg n ;
dom ((MSAlg h) # y) = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def 6
.= dom (h * y) by A7, A19, FINSEQ_3:120 ;
hence (MSAlg h) # y = h * y by A18, A15, A8, FINSEQ_1:13; :: thesis: verum