let R be non empty Poset; :: thesis: for A being OrderSortedSet of R

for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let A be OrderSortedSet of R; :: thesis: for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let B be V2() OrderSortedSet of R; :: thesis: for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let F be ManySortedFunction of A,B; :: thesis: ( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 ; :: thesis: F is order-sorted

let s1, s2 be Element of R; :: according to OSALG_3:def 1 :: thesis: ( s1 <= s2 implies for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )

assume A4: s1 <= s2 ; :: thesis: for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )

A5: ( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by FUNCT_2:def 1;

let a1 be set ; :: thesis: ( a1 in dom (F . s1) implies ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )

assume A6: a1 in dom (F . s1) ; :: thesis: ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )

A . s1 c= A . s2 by A4, OSALG_1:def 16;

hence a1 in dom (F . s2) by A6, A5; :: thesis: (F . s1) . a1 = (F . s2) . a1

thus (F . s1) . a1 = (F . s2) . a1 by A3, A4, A6; :: thesis: verum

for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let A be OrderSortedSet of R; :: thesis: for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let B be V2() OrderSortedSet of R; :: thesis: for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

let F be ManySortedFunction of A,B; :: thesis: ( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

hereby :: thesis: ( ( for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 ) implies F is order-sorted )

assume A3:
for s1, s2 being Element of R st s1 <= s2 holds for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 ) implies F is order-sorted )

assume A1:
F is order-sorted
; :: thesis: for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1

let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

assume A2: s1 <= s2 ; :: thesis: for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1

let a1 be set ; :: thesis: ( a1 in A . s1 implies (F . s1) . a1 = (F . s2) . a1 )

assume a1 in A . s1 ; :: thesis: (F . s1) . a1 = (F . s2) . a1

then a1 in dom (F . s1) by FUNCT_2:def 1;

hence (F . s1) . a1 = (F . s2) . a1 by A1, A2; :: thesis: verum

end;for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1

let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

assume A2: s1 <= s2 ; :: thesis: for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1

let a1 be set ; :: thesis: ( a1 in A . s1 implies (F . s1) . a1 = (F . s2) . a1 )

assume a1 in A . s1 ; :: thesis: (F . s1) . a1 = (F . s2) . a1

then a1 in dom (F . s1) by FUNCT_2:def 1;

hence (F . s1) . a1 = (F . s2) . a1 by A1, A2; :: thesis: verum

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 ; :: thesis: F is order-sorted

let s1, s2 be Element of R; :: according to OSALG_3:def 1 :: thesis: ( s1 <= s2 implies for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )

assume A4: s1 <= s2 ; :: thesis: for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )

A5: ( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by FUNCT_2:def 1;

let a1 be set ; :: thesis: ( a1 in dom (F . s1) implies ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )

assume A6: a1 in dom (F . s1) ; :: thesis: ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )

A . s1 c= A . s2 by A4, OSALG_1:def 16;

hence a1 in dom (F . s2) by A6, A5; :: thesis: (F . s1) . a1 = (F . s2) . a1

thus (F . s1) . a1 = (F . s2) . a1 by A3, A4, A6; :: thesis: verum