defpred S₁[ set , set ] 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 set st x in (((OSClass R) # ) * the Arity of S) . o holds
ex y being set 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 set ; :: thesis: ( x in (((OSClass R) # ) * the Arity of S) . o implies ex y being set 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 set 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 Th15;
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 4;
then A4: ((OSClass R) * the ResultSort of S) . o = (OSClass R) . (the ResultSort of S . o) by FUNCT_1:22
.= (OSClass R) . (the_result_sort_of o) by MSUALG_1:def 7 ;
o in dom (the Sorts of A * the ResultSort of S) by A3, PARTFUN1:def 4;
then A5: (the Sorts of A * the ResultSort of S) . o = the Sorts of A . (the ResultSort of S . o) by FUNCT_1:22
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 7 ;
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 10;
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:46;
(OSQuotRes R,o) . ((Den o,A) . a) in rng (OSQuotRes R,o) by A6, FUNCT_1:def 5;
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:22; :: 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 10;
A8: ((OSQuotRes R,o) * (Den o,A)) . b = (OSQuotRes R,o) . db by A7, FUNCT_1:22
.= OSClass R,db by Def16
.= 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, Def15;
hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, Th13; :: 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:28, MSUALG_4:def 6;
then A11: [da,db] in CompClass R,(CComp (the_result_sort_of o)) by Def11;
A12: da in the Sorts of A -carrier_of (CComp (the_result_sort_of o)) by Th6;
y = (OSQuotRes R,o) . ((Den o,A) . a) by A7, FUNCT_1:22
.= OSClass R,da by Def16
.= 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:44; :: 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 set st x in (((OSClass R) # ) * the Arity of S) . o holds
S₁[x,f . x] ) ) from WELLORD2:sch 1(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:4;
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