defpred S1[ object , object ] means for a being Element of Args (o,A) st $1 = R #_os a holds
$2 = ((OSQuotRes (R,o)) * (Den (o,A))) . a;
set Ca = (((OSClass R) #) * the Arity of S) . o;
set Cr = ((OSClass R) * the ResultSort of S) . o;
A1:
for x being object st x in (((OSClass R) #) * the Arity of S) . o holds
ex y being object st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
proof
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
let x be
object ;
( x in (((OSClass R) #) * the Arity of S) . o implies ex y being object st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) )
assume
x in (((OSClass R) #) * the Arity of S) . o
;
ex y being object st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
then consider a being
Element of
Args (
o,
A)
such that A2:
x = R #_os a
by Th14;
take y =
((OSQuotRes (R,o)) * (Den (o,A))) . a;
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
A3:
o in the
carrier' of
S
;
then
o in dom ((OSClass R) * the ResultSort of S)
by PARTFUN1:def 2;
then A4:
((OSClass R) * the ResultSort of S) . o =
(OSClass R) . ( the ResultSort of S . o)
by FUNCT_1:12
.=
(OSClass R) . (the_result_sort_of o)
by MSUALG_1:def 2
;
o in dom ( the Sorts of A * the ResultSort of S)
by A3, PARTFUN1:def 2;
then A5:
( the Sorts of A * the ResultSort of S) . o =
the
Sorts of
A . ( the ResultSort of S . o)
by FUNCT_1:12
.=
the
Sorts of
A . (the_result_sort_of o)
by MSUALG_1:def 2
;
then A6:
(
dom (OSQuotRes (R,o)) = the
Sorts of
A . (the_result_sort_of o) &
Result (
o,
A)
= the
Sorts of
A . (the_result_sort_of o) )
by FUNCT_2:def 1, MSUALG_1:def 5;
rng (Den (o,A)) c= Result (
o,
A)
;
then A7:
(
dom (Den (o,A)) = Args (
o,
A) &
dom ((OSQuotRes (R,o)) * (Den (o,A))) = dom (Den (o,A)) )
by A6, FUNCT_2:def 1, RELAT_1:27;
(OSQuotRes (R,o)) . ((Den (o,A)) . a) in rng (OSQuotRes (R,o))
by A6, FUNCT_1:def 3;
then
(OSQuotRes (R,o)) . ((Den (o,A)) . a) in (OSClass R) . (the_result_sort_of o)
by A4;
hence
y in ((OSClass R) * the ResultSort of S) . o
by A4, A7, FUNCT_1:12;
S1[x,y]
let b be
Element of
Args (
o,
A);
( x = R #_os b implies y = ((OSQuotRes (R,o)) * (Den (o,A))) . b )
reconsider da =
(Den (o,A)) . a,
db =
(Den (o,A)) . b as
Element of the
Sorts of
A . (the_result_sort_of o) by A5, MSUALG_1:def 5;
A8:
((OSQuotRes (R,o)) * (Den (o,A))) . b =
(OSQuotRes (R,o)) . db
by A7, FUNCT_1:12
.=
OSClass (
R,
db)
by Def14
.=
Class (
(CompClass (R,(CComp (the_result_sort_of o)))),
db)
;
assume A9:
x = R #_os b
;
y = ((OSQuotRes (R,o)) * (Den (o,A))) . b
for
n being
Nat st
n in dom a holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n)
then
(
the_result_sort_of o in CComp (the_result_sort_of o) &
[da,db] in R . (the_result_sort_of o) )
by EQREL_1:20, MSUALG_4:def 4;
then A11:
[da,db] in CompClass (
R,
(CComp (the_result_sort_of o)))
by Def9;
A12:
da in the
Sorts of
A -carrier_of (CComp (the_result_sort_of o))
by Th5;
y =
(OSQuotRes (R,o)) . ((Den (o,A)) . a)
by A7, FUNCT_1:12
.=
OSClass (
R,
da)
by Def14
.=
Class (
(CompClass (R,(CComp (the_result_sort_of o)))),
da)
;
hence
y = ((OSQuotRes (R,o)) * (Den (o,A))) . b
by A12, A8, A11, EQREL_1:35;
verum
end;
consider f being Function such that
A13:
( dom f = (((OSClass R) #) * the Arity of S) . o & rng f c= ((OSClass R) * the ResultSort of S) . o & ( for x being object st x in (((OSClass R) #) * the Arity of S) . o holds
S1[x,f . x] ) )
from FUNCT_1:sch 6(A1);
reconsider f = f as Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) by A13, FUNCT_2:2;
take
f
; for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
f . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a
thus
for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
f . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a
by A13; verum