let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for U1 being MSAlgebra of 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 of 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 of 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:10;
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 set 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 set 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 set st y in dom f holds
f . y = g . y
proof
let y be
set ;
( 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 4;
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:46;
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:22;
then A9:
f . n in the
Sorts of
U1 . ((the_arity_of o) /. n)
by A5, A7, PARTFUN1:def 8;
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:35;
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:9; verum