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 * ()) by PRALG_2:3;
then consider g being Function such that
A3: Fx = g and
dom g = dom ( the Sorts of U1 * ()) and
for x being object st x in dom ( the Sorts of U1 * ()) holds
g . x in ( the Sorts of U1 * ()) . x by CARD_3:def 5;
consider f being Function such that
A4: x = f and
dom f = dom ( the Sorts of U1 * ()) and
for x being object st x in dom ( the Sorts of U1 * ()) holds
f . x in ( the Sorts of U1 * ()) . x by ;
A5: dom f = dom () by A4, A3, Th6;
A6: for y being object st y in dom f holds
f . y = g . y
proof
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 = () /. n;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then rng () c= dom the Sorts of U1 by FINSEQ_1:def 4;
then A8: dom ( the Sorts of U1 * ()) = dom () by RELAT_1:27;
then f . n in ( the Sorts of U1 * ()) . n by A1, A4, A5, A7, Th6;
then f . n in the Sorts of U1 . (() . n) by ;
then A9: f . n in the Sorts of U1 . (() /. n) by ;
A10: (id the Sorts of U1) . (() /. n) = id ( the Sorts of U1 . (() /. n)) by Def1;
g . n = ((id the Sorts of U1) . (() /. n)) . (f . n) by A4, A3, A7, Lm1;
hence f . y = g . y by ; :: thesis: verum
end;
dom g = dom () by ;
hence x = (id the Sorts of U1) # x by ; :: thesis: verum