set qa = QuotOSAlg (U1,R);
set cqa = the Sorts of (QuotOSAlg (U1,R));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S1[ object , object ] means for a being Element of the Sorts of U1 . s st $1 = OSClass (R,a) holds
$2 = (F . s) . a;
A4:
the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s)
by Def11;
A5:
for x being object st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
ex y being object st
( y in the Sorts of U2 . s & S1[x,y] )
proof
let x be
object ;
( x in the Sorts of (QuotOSAlg (U1,R)) . s implies ex y being object st
( y in the Sorts of U2 . s & S1[x,y] ) )
A6:
R . s c= (OSCng F) . s
by A3, PBOOLE:def 2;
assume
x in the
Sorts of
(QuotOSAlg (U1,R)) . s
;
ex y being object st
( y in the Sorts of U2 . s & S1[x,y] )
then consider a being
set such that A7:
a in the
Sorts of
U1 . s
and A8:
x = Class (
(CompClass (R,(CComp s))),
a)
by A4, Def10;
reconsider a =
a as
Element of the
Sorts of
U1 . s by A7;
take y =
(F . s) . a;
( y in the Sorts of U2 . s & S1[x,y] )
thus
y in the
Sorts of
U2 . s
;
S1[x,y]
let b be
Element of the
Sorts of
U1 . s;
( x = OSClass (R,b) implies y = (F . s) . b )
assume A9:
x = OSClass (
R,
b)
;
y = (F . s) . b
x = OSClass (
R,
a)
by A8;
then
[b,a] in R . s
by A9, Th12;
then
[b,a] in (OSCng F) . s
by A6;
then
[b,a] in (MSCng F) . s
by A1, A2, Def23;
then
[b,a] in MSCng (
F,
s)
by A1, MSUALG_4:def 18;
hence
y = (F . s) . b
by MSUALG_4:def 17;
verum
end;
consider G being Function such that
A10:
( dom G = the Sorts of (QuotOSAlg (U1,R)) . s & rng G c= the Sorts of U2 . s & ( for x being object st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
S1[x,G . x] ) )
from FUNCT_1:sch 6(A5);
reconsider G = G as Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) by A10, FUNCT_2:def 1, RELSET_1:4;
take
G
; for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x
let a be Element of the Sorts of U1 . s; G . (OSClass (R,a)) = (F . s) . a
thus
G . (OSClass (R,a)) = (F . s) . a
by A4, A10; verum