let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: 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); :: thesis: 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

hence x = (id the Sorts of U1) # x by A4, A3, A6, Th6, FUNCT_1:2; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: 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); :: thesis: 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

dom g = dom (the_arity_of o)
by A3, Th6;
let y be object ; :: thesis: ( y in dom f implies f . y = g . y )

assume A7: y in dom f ; :: thesis: 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; :: thesis: verum

end;assume A7: y in dom f ; :: thesis: 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; :: thesis: verum

hence x = (id the Sorts of U1) # x by A4, A3, A6, Th6, FUNCT_1:2; :: thesis: verum