defpred S₁[ object , object ] 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 object st x in (((Class R) #) * the Arity of S) . o holds
ex y being object 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 object ; :: thesis: ( x in (((Class R) #) * the Arity of S) . o implies ex y being object 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 object 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 2;
then A4: ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by FUNCT_1:12
.= (Class 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 (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 5;
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:27;
(QuotRes (R,o)) . ((Den (o,A)) . a) in rng (QuotRes (R,o)) by A6, FUNCT_1:def 3;
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:12; :: 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 5;
A8: ((QuotRes (R,o)) * (Den (o,A))) . b = (QuotRes (R,o)) . db by A7, FUNCT_1:12
.= Class (R,db) by Def8
.= 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, Def7;
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
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:27;
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:12
.= the Sorts of A . ((the_arity_of o) /. n) by A11, A10, PARTFUN1:def 6 ;
hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, A14, A12, EQREL_1:35; :: thesis: verum

end;

then A15: [da,db] in R . (the_result_sort_of o) by Def4;
y = (QuotRes (R,o)) . ((Den (o,A)) . a) by A7, FUNCT_1:12
.= Class (R,da) by Def8
.= Class ((R . (the_result_sort_of o)),da) ;
hence y = ((QuotRes (R,o)) * (Den (o,A))) . b by A8, A15, EQREL_1:35; :: 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 object st x in (((Class R) #) * the Arity of S) . o holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(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:2;
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