let U1, U2 be Universal_Algebra; 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; ( 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
; 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); 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)); (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 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;
( 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
;
(MSAlg h) . ((the_arity_of o) /. m) = hthen
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
;
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; verum