defpred S₁[ set , set ] means for a being Element of Args o,A st $1 = R # a holds
$2 = ((QuotRes R,o) * (Den o,A)) . a;
set Ca = (((Class R) # ) * the Arity of S) . o;
set Cr = ((Class R) * the ResultSort of S) . o;
A1: for x being set st x in (((Class R) # ) * the Arity of S) . o holds
ex y being set st
( y in ((Class 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 (((Class R) # ) * the Arity of S) . o implies ex y being set st
( y in ((Class R) * the ResultSort of S) . o & S₁[x,y] ) )
assume x in (((Class R) # ) * the Arity of S) . o ; :: thesis: ex y being set st
( y in ((Class R) * the ResultSort of S) . o & S₁[x,y] )
then consider a being Element of Args o,A such that
A2: x = R # a by Th2;
take y = ((QuotRes R,o) * (Den o,A)) . a; :: thesis: ( y in ((Class R) * the ResultSort of S) . o & S₁[x,y] )
A3: o in the carrier' of S ;
then o in dom ((Class R) * the ResultSort of S) by PARTFUN1:def 4;
then A4: ((Class R) * the ResultSort of S) . o = (Class R) . (the ResultSort of S . o) by FUNCT_1:22
.= (Class 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 (QuotRes 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 ((QuotRes R,o) * (Den o,A)) = dom (Den o,A) ) by A6, FUNCT_2:def 1, RELAT_1:46;
(QuotRes R,o) . ((Den o,A) . a) in rng (QuotRes R,o) by A6, FUNCT_1:def 5;
then (QuotRes R,o) . ((Den o,A) . a) in (Class R) . (the_result_sort_of o) by A4;
hence y in ((Class 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 # b implies y = ((QuotRes 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: ((QuotRes R,o) * (Den o,A)) . b = (QuotRes R,o) . db by A7, FUNCT_1:22
.= Class R,db by Def10
.= Class (R . (the_result_sort_of o)),db ;
assume A9: x = R # b ; :: thesis: y = ((QuotRes 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 A11: n in dom a ; :: thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n)
then A12: ( (R # a) . n = Class (R . ((the_arity_of o) /. n)),(a . n) & (R # b) . n = Class (R . ((the_arity_of o) /. n)),(b . n) ) by A10, Def9;
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 (the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
then A14: a . n in (the Sorts of A * (the_arity_of o)) . n by A11, A10, MSUALG_3:6;
(the Sorts of A * (the_arity_of o)) . n = the Sorts of A . ((the_arity_of o) . n) by A13, A11, A10, FUNCT_1:22
.= the Sorts of A . ((the_arity_of o) /. n) by A11, A10, PARTFUN1:def 8 ;
hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, A14, A12, EQREL_1:44; :: thesis: verum

end;

then A15: [da,db] in R . (the_result_sort_of o) by Def6;
y = (QuotRes R,o) . ((Den o,A) . a) by A7, FUNCT_1:22
.= Class R,da by Def10
.= Class (R . (the_result_sort_of o)),da ;
hence y = ((QuotRes R,o) * (Den o,A)) . b by A8, A15, EQREL_1:44; :: thesis: verum

end;

consider f being Function such that
A16: ( dom f = (((Class R) # ) * the Arity of S) . o & rng f c= ((Class R) * the ResultSort of S) . o & ( for x being set st x in (((Class R) # ) * the Arity of S) . o holds
S₁[x,f . x] ) ) from WELLORD2:sch 1(A1);
reconsider f = f as Function of ((((Class R) # ) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) by A16, FUNCT_2:4;
take f ; :: thesis: for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
f . (R # a) = ((QuotRes R,o) * (Den o,A)) . a
thus for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
f . (R # a) = ((QuotRes R,o) * (Den o,A)) . a by A16; :: thesis: verum