let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let o be OperSymbol of S; for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let A be non-empty MSAlgebra over S; for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let R be MSCongruence of A; for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let x be set ; ( x in (((Class R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R # a )
assume A1:
x in (((Class R) #) * the Arity of S) . o
; ex a being Element of Args (o,A) st x = R # a
set ar = the_arity_of o;
A2:
the_arity_of o = the Arity of S . o
by MSUALG_1:def 1;
then
(((Class R) #) * the Arity of S) . o = product ((Class R) * (the_arity_of o))
by MSAFREE:1;
then consider f being Function such that
A3:
f = x
and
A4:
dom f = dom ((Class R) * (the_arity_of o))
and
A5:
for y being object st y in dom ((Class R) * (the_arity_of o)) holds
f . y in ((Class R) * (the_arity_of o)) . y
by A1, CARD_3:def 5;
defpred S1[ object , object ] means $2 in f . $1;
A6:
dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 2;
A7:
for n being Nat st n in dom f holds
f . n in Class (R . ((the_arity_of o) /. n))
A9:
for a being object st a in dom f holds
ex b being object st S1[a,b]
consider g being Function such that
A12:
( dom g = dom f & ( for a being object st a in dom f holds
S1[a,g . a] ) )
from CLASSES1:sch 1(A9);
dom the Sorts of A = the carrier of S
by PARTFUN1:def 2;
then
rng (the_arity_of o) c= dom the Sorts of A
;
then A13:
dom g = dom ( the Sorts of A * (the_arity_of o))
by A4, A6, A12, RELAT_1:27;
A14:
for y being object st y in dom ( the Sorts of A * (the_arity_of o)) holds
g . y in ( the Sorts of A * (the_arity_of o)) . y
proof
let y be
object ;
( y in dom ( the Sorts of A * (the_arity_of o)) implies g . y in ( the Sorts of A * (the_arity_of o)) . y )
assume A15:
y in dom ( the Sorts of A * (the_arity_of o))
;
g . y in ( the Sorts of A * (the_arity_of o)) . y
then A16:
(
g . y in f . y &
f . y in ((Class R) * (the_arity_of o)) . y )
by A4, A5, A12, A13;
reconsider n =
y as
Nat by A15, ORDINAL1:def 12;
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
A17:
(the_arity_of o) . n = (the_arity_of o) /. n
by A4, A6, A12, A13, A15, PARTFUN1:def 6;
then ((Class R) * (the_arity_of o)) . y =
(Class R) . s
by A4, A12, A13, A15, FUNCT_1:12
.=
Class (R . s)
by Def6
;
then
g . n in the
Sorts of
A . s
by A16;
hence
g . y in ( the Sorts of A * (the_arity_of o)) . y
by A15, A17, FUNCT_1:12;
verum
end;
Args (o,A) =
(( the Sorts of A #) * the Arity of S) . o
by MSUALG_1:def 4
.=
product ( the Sorts of A * (the_arity_of o))
by A2, MSAFREE:1
;
then reconsider g = g as Element of Args (o,A) by A13, A14, CARD_3:9;
A18:
now for x being object st x in dom (the_arity_of o) holds
f . x = (R # g) . xlet x be
object ;
( x in dom (the_arity_of o) implies f . x = (R # g) . x )assume A19:
x in dom (the_arity_of o)
;
f . x = (R # g) . xthen reconsider n =
x as
Nat by ORDINAL1:def 12;
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
f . n in Class (R . s)
by A4, A6, A7, A19;
then consider a1 being
object such that A20:
a1 in the
Sorts of
A . s
and A21:
f . n = Class (
(R . s),
a1)
by EQREL_1:def 3;
g . n in f . n
by A4, A6, A12, A19;
then
Class (
(R . s),
(g . n))
= Class (
(R . s),
a1)
by A20, A21, EQREL_1:23;
hence
f . x = (R # g) . x
by A19, A21, Def7;
verum end;
take
g
; x = R # g
dom (R # g) = dom ((Class R) * (the_arity_of o))
by CARD_3:9;
hence
x = R # g
by A3, A4, A6, A18, FUNCT_1:2; verum