defpred S1[ object , object ] means ex f being ManySortedFunction of F2() . $1 st
( $2 = f & ( for r being Element of F1()
for t being Element of F2() . $1 holds
( dom (f . t) = F1() & (f . t) . r = F4($1,r,t) ) ) );
A2: for s being object st s in F1() holds
ex y being object st S1[s,y]
proof
let s be object ; :: thesis: ( s in F1() implies ex y being object st S1[s,y] )
assume s in F1() ; :: thesis: ex y being object st S1[s,y]
then reconsider s0 = s as Element of F1() ;
defpred S2[ object , object ] means ex g being Function st
( $2 = g & dom g = F1() & ( for r being Element of F1() holds g . r = F4(s,r,$1) ) );
A3: for t being object st t in F2() . s holds
ex y being object st S2[t,y]
proof
let t be object ; :: thesis: ( t in F2() . s implies ex y being object st S2[t,y] )
assume t in F2() . s ; :: thesis: ex y being object st S2[t,y]
deffunc H1( set ) -> set = F4(s,$1,t);
consider g being Function such that
A4: ( dom g = F1() & ( for r being Element of F1() holds g . r = H1(r) ) ) from FUNCT_1:sch 4();
 take g ; :: thesis: S2[t,g]
take g ; :: thesis: ( g = g & dom g = F1() & ( for r being Element of F1() holds g . r = F4(s,r,t) ) )
thus ( g = g & dom g = F1() & ( for r being Element of F1() holds g . r = F4(s,r,t) ) ) by A4; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = F2() . s & ( for t being object st t in F2() . s holds
S2[t,f . t] ) ) from CLASSES1:sch 1(A3);
 reconsider f = f as ManySortedSet of F2() . s by A5, RELAT_1:def 18, PARTFUN1:def 2;
f is Function-yielding
proof
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then S2[x,f . x] by A5;
hence f . x is set ; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of F2() . s ;
take f ; :: thesis: S1[s,f]
take f ; :: thesis: ( f = f & ( for r being Element of F1()
for t being Element of F2() . s holds
( dom (f . t) = F1() & (f . t) . r = F4(s,r,t) ) ) )
thus f = f ; :: thesis: for r being Element of F1()
for t being Element of F2() . s holds
( dom (f . t) = F1() & (f . t) . r = F4(s,r,t) )
let r be Element of F1(); :: thesis: for t being Element of F2() . s holds
( dom (f . t) = F1() & (f . t) . r = F4(s,r,t) )
let t be Element of F2() . s; :: thesis: ( dom (f . t) = F1() & (f . t) . r = F4(s,r,t) )
t in F2() . s0 ;
then S2[t,f . t] by A5;
hence ( dom (f . t) = F1() & (f . t) . r = F4(s,r,t) ) ; :: thesis: verum
end;
consider F being Function such that
A6: ( dom F = F1() & ( for x being object st x in F1() holds
S1[x,F . x] ) ) from CLASSES1:sch 1(A2);
 reconsider F = F as ManySortedSet of F1() by A6, RELAT_1:def 18, PARTFUN1:def 2;
F is Function-yielding
proof
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 F or F . x is set )
assume x in dom F ; :: thesis: F . x is set
then S1[x,F . x] by A6;
hence F . x is set ; :: thesis: verum
end;
then reconsider F = F as ManySortedFunction of F1() ;
F is ManySortedMSSet of F2(),F1()
proof
let i, j be set ; :: according to AOFA_A00:def 6 :: thesis: ( i in F1() implies ( dom (F . i) = F2() . i & ( j in F2() . i implies (F . i) . j is ManySortedSet of F1() ) ) )
assume i in F1() ; :: thesis: ( dom (F . i) = F2() . i & ( j in F2() . i implies (F . i) . j is ManySortedSet of F1() ) )
then consider f being ManySortedFunction of F2() . i such that
A7: ( F . i = f & ( for r being Element of F1()
for t being Element of F2() . i holds
( dom (f . t) = F1() & (f . t) . r = F4(i,r,t) ) ) ) by A6;
thus dom (F . i) = F2() . i by A7, PARTFUN1:def 2; :: thesis: ( j in F2() . i implies (F . i) . j is ManySortedSet of F1() )
assume j in F2() . i ; :: thesis: (F . i) . j is ManySortedSet of F1()
then dom (f . j) = F1() by A7;
hence (F . i) . j is ManySortedSet of F1() by A7, RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum
end;
then reconsider F = F as ManySortedMSSet of F2(),F1() ;
F is ManySortedMSSet of F2(),F3()
proof
let i, a be set ; :: according to AOFA_A00:def 7 :: thesis: ( i in F1() & a in F2() . i implies (F . i) . a is ManySortedSubset of F3() )
assume A8: ( i in F1() & a in F2() . i ) ; :: thesis: (F . i) . a is ManySortedSubset of F3()
then reconsider g = (F . i) . a as ManySortedSet of F1() by Def6;
consider f being ManySortedFunction of F2() . i such that
A9: ( F . i = f & ( for r being Element of F1()
for t being Element of F2() . i holds
( dom (f . t) = F1() & (f . t) . r = F4(i,r,t) ) ) ) by A6, A8;
g is ManySortedSubset of F3()
proof
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in F1() or g . x c= F3() . x )
assume x in F1() ; :: thesis: g . x c= F3() . x
then ( g . x = F4(i,x,a) & F4(i,x,a) is Subset of (F3() . x) ) by A1, A8, A9;
hence g . x c= F3() . x ; :: thesis: verum
end;
hence (F . i) . a is ManySortedSubset of F3() ; :: thesis: verum
end;
then reconsider F = F as ManySortedMSSet of F2(),F3() ;
take F ; :: thesis: for s, r being Element of F1()
for t being Element of F2() . s holds ((F . s) . t) . r = F4(s,r,t)
let s, r be Element of F1(); :: thesis: for t being Element of F2() . s holds ((F . s) . t) . r = F4(s,r,t)
let t be Element of F2() . s; :: thesis: ((F . s) . t) . r = F4(s,r,t)
S1[s,F . s] by A6;
hence ((F . s) . t) . r = F4(s,r,t) ; :: thesis: verum