let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
let o be OperSymbol of S; for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
let U1 be MSAlgebra over S; ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x )
set F = id the Sorts of U1;
assume A1:
Args (o,U1) <> {}
; for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
then reconsider AA = Args (o,U1) as non empty set ;
let x be Element of Args (o,U1); x = (id the Sorts of U1) # x
reconsider Fx = (id the Sorts of U1) # x as Element of AA ;
A2:
Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:3;
then consider g being Function such that
A3:
Fx = g
and
dom g = dom ( the Sorts of U1 * (the_arity_of o))
and
for x being object st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
g . x in ( the Sorts of U1 * (the_arity_of o)) . x
by CARD_3:def 5;
consider f being Function such that
A4:
x = f
and
dom f = dom ( the Sorts of U1 * (the_arity_of o))
and
for x being object st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
f . x in ( the Sorts of U1 * (the_arity_of o)) . x
by A1, A2, CARD_3:def 5;
A5:
dom f = dom (the_arity_of o)
by A4, A3, Th6;
A6:
for y being object st y in dom f holds
f . y = g . y
proof
let y be
object ;
( y in dom f implies f . y = g . y )
assume A7:
y in dom f
;
f . y = g . y
then reconsider n =
y as
Nat by A5;
set p =
(the_arity_of o) /. n;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then
rng (the_arity_of o) c= dom the
Sorts of
U1
by FINSEQ_1:def 4;
then A8:
dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
then
f . n in ( the Sorts of U1 * (the_arity_of o)) . n
by A1, A4, A5, A7, Th6;
then
f . n in the
Sorts of
U1 . ((the_arity_of o) . n)
by A5, A7, A8, FUNCT_1:12;
then A9:
f . n in the
Sorts of
U1 . ((the_arity_of o) /. n)
by A5, A7, PARTFUN1:def 6;
A10:
(id the Sorts of U1) . ((the_arity_of o) /. n) = id ( the Sorts of U1 . ((the_arity_of o) /. n))
by Def1;
g . n = ((id the Sorts of U1) . ((the_arity_of o) /. n)) . (f . n)
by A4, A3, A7, Lm1;
hence
f . y = g . y
by A10, A9, FUNCT_1:18;
verum
end;
dom g = dom (the_arity_of o)
by A3, Th6;
hence
x = (id the Sorts of U1) # x
by A4, A3, A6, Th6, FUNCT_1:2; verum