defpred S₁[ 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 & S₁[x,y] )

proof

set ro = the_result_sort_of o;
set ar = the_arity_of o;
let x be object ; :: thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex y being object st
( y in ((OSClass R) * the ResultSort of S) . o & S₁[x,y] ) )
assume x in (((OSClass R) #) * the Arity of S) . o ; :: thesis: ex y being object st
( y in ((OSClass R) * the ResultSort of S) . o & S₁[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; :: thesis: ( y in ((OSClass R) * the ResultSort of S) . o & S₁[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; :: thesis: S₁[x,y]
let b be Element of Args (o,A); :: thesis: ( 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 ; :: thesis: 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)

proof

let n be Nat; :: thesis: ( n in dom a implies [(a . n),(b . n)] in R . ((the_arity_of o) /. n) )
A10: dom a = dom (the_arity_of o) by MSUALG_3:6;
assume n in dom a ; :: thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n)
then ( ex ya being Element of the Sorts of A . ((the_arity_of o) /. n) st
( ya = a . n & (R #_os a) . n = OSClass (R,ya) ) & ex yb being Element of the Sorts of A . ((the_arity_of o) /. n) st
( yb = b . n & (R #_os b) . n = OSClass (R,yb) ) ) by A10, Def13;
hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, Th12; :: thesis: verum

end;

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; :: thesis: 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
S₁[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 ; :: thesis: 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; :: thesis: verum