defpred S_{1}[ object , object ] means ex f being ManySortedFunction of F_{2}() . $1 st

( $2 = f & ( for r being Element of F_{1}()

for t being Element of F_{2}() . $1 holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}($1,r,t) ) ) );

A2: for s being object st s in F_{1}() holds

ex y being object st S_{1}[s,y]

A6: ( dom F = F_{1}() & ( for x being object st x in F_{1}() holds

S_{1}[x,F . x] ) )
from CLASSES1:sch 1(A2);

reconsider F = F as ManySortedSet of F_{1}() by A6, RELAT_1:def 18, PARTFUN1:def 2;

F is Function-yielding_{1}() ;

F is ManySortedMSSet of F_{2}(),F_{1}()
_{2}(),F_{1}() ;

F is ManySortedMSSet of F_{2}(),F_{3}()
_{2}(),F_{3}() ;

take F ; :: thesis: for s, r being Element of F_{1}()

for t being Element of F_{2}() . s holds ((F . s) . t) . r = F_{4}(s,r,t)

let s, r be Element of F_{1}(); :: thesis: for t being Element of F_{2}() . s holds ((F . s) . t) . r = F_{4}(s,r,t)

let t be Element of F_{2}() . s; :: thesis: ((F . s) . t) . r = F_{4}(s,r,t)

S_{1}[s,F . s]
by A6;

hence ((F . s) . t) . r = F_{4}(s,r,t)
; :: thesis: verum

( $2 = f & ( for r being Element of F

for t being Element of F

( dom (f . t) = F

A2: for s being object st s in F

ex y being object st S

proof

consider F being Function such that
let s be object ; :: thesis: ( s in F_{1}() implies ex y being object st S_{1}[s,y] )

assume s in F_{1}()
; :: thesis: ex y being object st S_{1}[s,y]

then reconsider s0 = s as Element of F_{1}() ;

defpred S_{2}[ object , object ] means ex g being Function st

( $2 = g & dom g = F_{1}() & ( for r being Element of F_{1}() holds g . r = F_{4}(s,r,$1) ) );

A3: for t being object st t in F_{2}() . s holds

ex y being object st S_{2}[t,y]

A5: ( dom f = F_{2}() . s & ( for t being object st t in F_{2}() . s holds

S_{2}[t,f . t] ) )
from CLASSES1:sch 1(A3);

reconsider f = f as ManySortedSet of F_{2}() . s by A5, RELAT_1:def 18, PARTFUN1:def 2;

f is Function-yielding_{2}() . s ;

take f ; :: thesis: S_{1}[s,f]

take f ; :: thesis: ( f = f & ( for r being Element of F_{1}()

for t being Element of F_{2}() . s holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(s,r,t) ) ) )

thus f = f ; :: thesis: for r being Element of F_{1}()

for t being Element of F_{2}() . s holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(s,r,t) )

let r be Element of F_{1}(); :: thesis: for t being Element of F_{2}() . s holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(s,r,t) )

let t be Element of F_{2}() . s; :: thesis: ( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(s,r,t) )

t in F_{2}() . s0
;

then S_{2}[t,f . t]
by A5;

hence ( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(s,r,t) )
; :: thesis: verum

end;assume s in F

then reconsider s0 = s as Element of F

defpred S

( $2 = g & dom g = F

A3: for t being object st t in F

ex y being object st S

proof

consider f being Function such that
let t be object ; :: thesis: ( t in F_{2}() . s implies ex y being object st S_{2}[t,y] )

assume t in F_{2}() . s
; :: thesis: ex y being object st S_{2}[t,y]

deffunc H_{1}( set ) -> set = F_{4}(s,$1,t);

consider g being Function such that

A4: ( dom g = F_{1}() & ( for r being Element of F_{1}() holds g . r = H_{1}(r) ) )
from FUNCT_1:sch 4();

take g ; :: thesis: S_{2}[t,g]

take g ; :: thesis: ( g = g & dom g = F_{1}() & ( for r being Element of F_{1}() holds g . r = F_{4}(s,r,t) ) )

thus ( g = g & dom g = F_{1}() & ( for r being Element of F_{1}() holds g . r = F_{4}(s,r,t) ) )
by A4; :: thesis: verum

end;assume t in F

deffunc H

consider g being Function such that

A4: ( dom g = F

take g ; :: thesis: S

take g ; :: thesis: ( g = g & dom g = F

thus ( g = g & dom g = F

A5: ( dom f = F

S

reconsider f = f as ManySortedSet of F

f is Function-yielding

proof

then reconsider f = f as ManySortedFunction of F
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 S_{2}[x,f . x]
by A5;

hence f . x is set ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x is set

then S

hence f . x is set ; :: thesis: verum

take f ; :: thesis: S

take f ; :: thesis: ( f = f & ( for r being Element of F

for t being Element of F

( dom (f . t) = F

thus f = f ; :: thesis: for r being Element of F

for t being Element of F

( dom (f . t) = F

let r be Element of F

( dom (f . t) = F

let t be Element of F

t in F

then S

hence ( dom (f . t) = F

A6: ( dom F = F

S

reconsider F = F as ManySortedSet of F

F is Function-yielding

proof

then reconsider F = F as ManySortedFunction of F
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 S_{1}[x,F . x]
by A6;

hence F . x is set ; :: thesis: verum

end;assume x in dom F ; :: thesis: F . x is set

then S

hence F . x is set ; :: thesis: verum

F is ManySortedMSSet of F

proof

then reconsider F = F as ManySortedMSSet of F
let i, j be set ; :: according to AOFA_A00:def 6 :: thesis: ( i in F_{1}() implies ( dom (F . i) = F_{2}() . i & ( j in F_{2}() . i implies (F . i) . j is ManySortedSet of F_{1}() ) ) )

assume i in F_{1}()
; :: thesis: ( dom (F . i) = F_{2}() . i & ( j in F_{2}() . i implies (F . i) . j is ManySortedSet of F_{1}() ) )

then consider f being ManySortedFunction of F_{2}() . i such that

A7: ( F . i = f & ( for r being Element of F_{1}()

for t being Element of F_{2}() . i holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(i,r,t) ) ) )
by A6;

thus dom (F . i) = F_{2}() . i
by A7, PARTFUN1:def 2; :: thesis: ( j in F_{2}() . i implies (F . i) . j is ManySortedSet of F_{1}() )

assume j in F_{2}() . i
; :: thesis: (F . i) . j is ManySortedSet of F_{1}()

then dom (f . j) = F_{1}()
by A7;

hence (F . i) . j is ManySortedSet of F_{1}()
by A7, RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum

end;assume i in F

then consider f being ManySortedFunction of F

A7: ( F . i = f & ( for r being Element of F

for t being Element of F

( dom (f . t) = F

thus dom (F . i) = F

assume j in F

then dom (f . j) = F

hence (F . i) . j is ManySortedSet of F

F is ManySortedMSSet of F

proof

then reconsider F = F as ManySortedMSSet of F
let i, a be set ; :: according to AOFA_A00:def 7 :: thesis: ( i in F_{1}() & a in F_{2}() . i implies (F . i) . a is ManySortedSubset of F_{3}() )

assume A8: ( i in F_{1}() & a in F_{2}() . i )
; :: thesis: (F . i) . a is ManySortedSubset of F_{3}()

then reconsider g = (F . i) . a as ManySortedSet of F_{1}() by Def6;

consider f being ManySortedFunction of F_{2}() . i such that

A9: ( F . i = f & ( for r being Element of F_{1}()

for t being Element of F_{2}() . i holds

( dom (f . t) = F_{1}() & (f . t) . r = F_{4}(i,r,t) ) ) )
by A6, A8;

g is ManySortedSubset of F_{3}()
_{3}()
; :: thesis: verum

end;assume A8: ( i in F

then reconsider g = (F . i) . a as ManySortedSet of F

consider f being ManySortedFunction of F

A9: ( F . i = f & ( for r being Element of F

for t being Element of F

( dom (f . t) = F

g is ManySortedSubset of F

proof

hence
(F . i) . a is ManySortedSubset of F
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in F_{1}() or g . x c= F_{3}() . x )

assume x in F_{1}()
; :: thesis: g . x c= F_{3}() . x

then ( g . x = F_{4}(i,x,a) & F_{4}(i,x,a) is Subset of (F_{3}() . x) )
by A1, A8, A9;

hence g . x c= F_{3}() . x
; :: thesis: verum

end;assume x in F

then ( g . x = F

hence g . x c= F

take F ; :: thesis: for s, r being Element of F

for t being Element of F

let s, r be Element of F

let t be Element of F

S

hence ((F . s) . t) . r = F