let R be non empty Poset; 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; 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; 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; ( 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 ( ( 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
;
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) . a1let s1,
s2 be
Element of
R;
( s1 <= s2 implies for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1 )assume A2:
s1 <= s2
;
for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1let a1 be
set ;
( a1 in A . s1 implies (F . s1) . a1 = (F . s2) . a1 )assume
a1 in A . s1
;
(F . s1) . a1 = (F . s2) . a1then
a1 in dom (F . s1)
by FUNCT_2:def 1;
hence
(F . s1) . a1 = (F . s2) . a1
by A1, A2;
verum
end;
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
; F is order-sorted
let s1, s2 be Element of R; OSALG_3:def 1 ( 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
; 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 ; ( a1 in dom (F . s1) implies ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )
assume A6:
a1 in dom (F . s1)
; ( 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; (F . s1) . a1 = (F . s2) . a1
thus
(F . s1) . a1 = (F . s2) . a1
by A3, A4, A6; verum