let S be locally_directed OrderSortedSign; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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
; :: thesis: 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 6;
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 & dom f = dom ((OSClass R) * (the_arity_of o)) & ( for y being set 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;
A4:
dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 4;
A5:
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;
:: thesis: ( n in dom f implies f . n in OSClass R,((the_arity_of o) /. n) )
assume A6:
n in dom f
;
:: thesis: f . n in OSClass R,((the_arity_of o) /. n)
then A7:
(the_arity_of o) . n = (the_arity_of o) /. n
by A3, A4, PARTFUN1:def 8;
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
((OSClass R) * (the_arity_of o)) . n =
(OSClass R) . s
by A3, A6, A7, FUNCT_1:22
.=
OSClass R,
s
by Def13
;
hence
f . n in OSClass R,
((the_arity_of o) /. n)
by A3, A6;
:: thesis: verum
end;
defpred S1[ set , set ] means ( $2 in the Sorts of A . ((the_arity_of o) /. $1) & $2 in f . $1 );
A8:
for a being set st a in dom f holds
ex b being set st S1[a,b]
proof
let a be
set ;
:: thesis: ( a in dom f implies ex b being set st S1[a,b] )
assume A9:
a in dom f
;
:: thesis: ex b being set st S1[a,b]
then reconsider n =
a as
Nat by A3;
reconsider s =
(the_arity_of o) /. a as
Element of
S ;
f . n in OSClass R,
s
by A5, A9;
then consider x being
set such that A10:
(
x in the
Sorts of
A . s &
f . n = Class (CompClass R,(CComp s)),
x )
by Def12;
take
x
;
:: thesis: S1[a,x]
thus
S1[
a,
x]
by A10, Th6, EQREL_1:28;
:: thesis: verum
end;
consider g being Function such that
A11:
( dom g = dom f & ( for a being set st a in dom f holds
S1[a,g . a] ) )
from CLASSES1:sch 1(A8);
A12: Args o,A =
((the Sorts of A # ) * the Arity of S) . o
by MSUALG_1:def 9
.=
product (the Sorts of A * (the_arity_of o))
by A2, MSAFREE:1
;
dom the Sorts of A = the carrier of S
by PARTFUN1:def 4;
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 A3, A4, A11, RELAT_1:46;
for y being set 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
then reconsider g = g as Element of Args o,A by A12, A13, CARD_3:18;
take
g
; :: thesis: x = R #_os g
A16:
dom (R #_os g) = dom ((OSClass R) * (the_arity_of o))
by CARD_3:18;
for x being set st x in dom (the_arity_of o) holds
f . x = (R #_os g) . x
proof
let x be
set ;
:: thesis: ( x in dom (the_arity_of o) implies f . x = (R #_os g) . x )
assume A17:
x in dom (the_arity_of o)
;
:: thesis: f . x = (R #_os g) . x
then reconsider n =
x as
Nat ;
reconsider s =
(the_arity_of o) /. n as
Element of
S ;
consider z being
Element of the
Sorts of
A . ((the_arity_of o) /. n) such that A18:
(
z = g . n &
(R #_os g) . n = OSClass R,
z )
by A17, Def15;
A19:
(
g . n in the
Sorts of
A . ((the_arity_of o) /. n) &
g . n in f . n )
by A3, A4, A11, A17;
f . n in OSClass R,
s
by A3, A4, A5, A17;
then consider u being
set such that A20:
(
u in the
Sorts of
A . s &
f . n = Class (CompClass R,(CComp s)),
u )
by Def12;
u in the
Sorts of
A -carrier_of (CComp s)
by A20, Th6;
hence
f . x = (R #_os g) . x
by A18, A19, A20, EQREL_1:31;
:: thesis: verum
end;
hence
x = R #_os g
by A3, A4, A16, FUNCT_1:9; :: thesis: verum