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
then A2:
MSSign U1 = MSSign U2
by Th10;
A3:
0 in {0 }
by TARSKI:def 1;
set f = MSAlg h;
let o be OperSymbol of (MSSign U1); :: thesis: for y being Element of Args o,(MSAlg U1) holds (MSAlg h) # y = h * y
let y be Element of Args o,(MSAlg U1); :: thesis: (MSAlg h) # y = h * y
reconsider f1 = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A4:
( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = f1 & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 )
by MSUALG_1:def 13;
then A5:
the_arity_of o = ((*--> 0 ) * (signature U1)) . o
by MSUALG_1:def 6;
reconsider f2 = (*--> 0 ) * (signature U2) as Function of (dom (signature U2)),({0 } * ) by MSUALG_1:7;
A6:
( the carrier of (MSSign U2) = {0 } & the carrier' of (MSSign U2) = dom (signature U2) & the Arity of (MSSign U2) = f2 & the ResultSort of (MSSign U2) = (dom (signature U2)) --> 0 )
by MSUALG_1:def 13;
o in dom (signature U2)
by A2, A6;
then A7:
o in dom (signature U1)
by A1, UNIALG_2:def 2;
then
o in dom f1
by FUNCT_2:def 1;
then A8:
((*--> 0 ) * (signature U1)) . o = (*--> 0 ) . ((signature U1) . o)
by FUNCT_1:22;
(signature U1) . o in rng (signature U1)
by A7, FUNCT_1:def 5;
then consider n being Element of NAT such that
A9:
n = (signature U1) . o
;
A10:
now let m be
Nat;
:: thesis: ( m in dom y implies (MSAlg h) . ((the_arity_of o) /. m) = h )assume
m in dom y
;
:: thesis: (MSAlg h) . ((the_arity_of o) /. m) = hthen A11:
m in dom (the_arity_of o)
by MSUALG_3:6;
0 is
Element of
{0 }
by TARSKI:def 1;
then
n |-> 0 is
FinSequence of
{0 }
by FINSEQ_2:77;
then reconsider l =
n |-> 0 as
Element of the
carrier of
(MSSign U1) * by A4, FINSEQ_1:def 11;
A12:
m in dom (n |-> 0 )
by A5, A8, A9, A11, PBOOLE:def 20;
A13:
(the_arity_of o) /. m = l /. m
by A5, A8, A9, PBOOLE:def 20;
A14:
l /. m = l . m
by A12, PARTFUN1:def 8;
dom (n |-> 0 ) = Seg n
by FUNCOP_1:19;
then
(the_arity_of o) /. m = 0
by A12, A13, A14, FUNCOP_1:13;
hence (MSAlg h) . ((the_arity_of o) /. m) =
(0 .--> h) . 0
by A1, Def3, Th10
.=
h
by A3, FUNCOP_1:13
;
:: thesis: verum end;
A15:
y is FinSequence of the carrier of U1
by Th14;
then A16:
rng y c= the carrier of U1
by FINSEQ_1:def 4;
A17: dom y =
dom (the_arity_of o)
by MSUALG_3:6
.=
dom (n |-> 0 )
by A5, A8, A9, PBOOLE:def 20
.=
Seg n
by FUNCOP_1:19
;
set X = dom (h * y);
A18: dom ((MSAlg h) # y) =
dom (the_arity_of o)
by MSUALG_3:6
.=
dom (n |-> 0 )
by A5, A8, A9, PBOOLE:def 20
.=
Seg n
by FUNCOP_1:19
.=
dom (h * y)
by A15, A17, ALG_1:1
;
dom ((MSAlg h) # y) =
dom (the_arity_of o)
by MSUALG_3:6
.=
dom (n |-> 0 )
by A5, A8, A9, PBOOLE:def 20
.=
Seg n
by FUNCOP_1:19
;
then A19:
(MSAlg h) # y is FinSequence
by FINSEQ_1:def 2;
dom h = the carrier of U1
by FUNCT_2:def 1;
then reconsider p = h * y as FinSequence by A15, A16, FINSEQ_1:20;
dom (h * y) = dom y
by A15, ALG_1:1;
hence
(MSAlg h) # y = h * y
by A18, A19, A20, FINSEQ_1:17; :: thesis: verum