let S be locally_directed OrderSortedSign; for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let o be Element of the carrier' of S; for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let A be non-empty OSAlgebra of S; for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let R be OSCongruence of A; for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let x be set ; ( x in (((OSClass R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R #_os a )
assume A1:
x in (((OSClass R) #) * the Arity of S) . o
; ex a being Element of Args (o,A) st x = R #_os a
set ar = the_arity_of o;
A2:
the_arity_of o = the Arity of S . o
by MSUALG_1:def 1;
then
(((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o))
by MSAFREE:1;
then consider f being Function such that
A3:
f = x
and
A4:
dom f = dom ((OSClass R) * (the_arity_of o))
and
A5:
for y being object st y in dom ((OSClass R) * (the_arity_of o)) holds
f . y in ((OSClass R) * (the_arity_of o)) . y
by A1, CARD_3:def 5;
defpred S1[ object , object ] means ( $2 in the Sorts of A . ((the_arity_of o) /. $1) & $2 in f . $1 );
A6:
dom ((OSClass 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 OSClass (R,((the_arity_of o) /. n))
proof
let n be
Nat;
( n in dom f implies f . n in OSClass (R,((the_arity_of o) /. n)) )
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
assume A8:
n in dom f
;
f . n in OSClass (R,((the_arity_of o) /. n))
then
(the_arity_of o) . n = (the_arity_of o) /. n
by A4, A6, PARTFUN1:def 6;
then ((OSClass R) * (the_arity_of o)) . n =
(OSClass R) . s
by A4, A8, FUNCT_1:12
.=
OSClass (
R,
s)
by Def11
;
hence
f . n in OSClass (
R,
((the_arity_of o) /. n))
by A4, A5, A8;
verum
end;
A9:
for a being object st a in dom f holds
ex b being object st S1[a,b]
proof
let a be
object ;
( a in dom f implies ex b being object st S1[a,b] )
reconsider s =
(the_arity_of o) /. a as
Element of
S ;
assume A10:
a in dom f
;
ex b being object st S1[a,b]
then reconsider n =
a as
Nat by A4;
f . n in OSClass (
R,
s)
by A7, A10;
then consider x being
set such that A11:
(
x in the
Sorts of
A . s &
f . n = Class (
(CompClass (R,(CComp s))),
x) )
by Def10;
take
x
;
S1[a,x]
thus
S1[
a,
x]
by A11, Th5, EQREL_1:20;
verum
end;
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
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;
A16:
for x being object st x in dom (the_arity_of o) holds
f . x = (R #_os g) . x
proof
let x be
object ;
( x in dom (the_arity_of o) implies f . x = (R #_os g) . x )
assume A17:
x in dom (the_arity_of o)
;
f . x = (R #_os g) . x
then reconsider n =
x as
Nat ;
A18:
( ex
z being
Element of the
Sorts of
A . ((the_arity_of o) /. n) st
(
z = g . n &
(R #_os g) . n = OSClass (
R,
z) ) &
g . n in f . n )
by A4, A6, A12, A17, Def13;
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
f . n in OSClass (
R,
s)
by A4, A6, A7, A17;
then consider u being
set such that A19:
u in the
Sorts of
A . s
and A20:
f . n = Class (
(CompClass (R,(CComp s))),
u)
by Def10;
u in the
Sorts of
A -carrier_of (CComp s)
by A19, Th5;
hence
f . x = (R #_os g) . x
by A18, A20, EQREL_1:23;
verum
end;
take
g
; x = R #_os g
dom (R #_os g) = dom ((OSClass R) * (the_arity_of o))
by CARD_3:9;
hence
x = R #_os g
by A3, A4, A6, A16, FUNCT_1:2; verum