let R be non empty Poset; for A being OrderSortedSet of R
for B, C being V2() OrderSortedSet of R
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted
let A be OrderSortedSet of R; for B, C being V2() OrderSortedSet of R
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted
let B, C be V2() OrderSortedSet of R; for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted
let F be ManySortedFunction of A,B; for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted
let G be ManySortedFunction of B,C; ( F is order-sorted & G is order-sorted implies G ** F is order-sorted )
assume that
A1:
F is order-sorted
and
A2:
G is order-sorted
; G ** 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
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
proof
let s1,
s2 be
Element of
R;
( s1 <= s2 implies for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A3:
s1 <= s2
;
for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
A4:
A . s1 c= A . s2
by A3, OSALG_1:def 16;
let a1 be
set ;
( a1 in A . s1 implies ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A5:
a1 in A . s1
;
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
A6:
(F . s1) . a1 = (F . s2) . a1
by A1, A3, A5, Th2;
(F . s1) . a1 in B . s1
by A5, FUNCT_2:5;
then A7:
(G . s1) . ((F . s2) . a1) = (G . s2) . ((F . s2) . a1)
by A2, A3, A6, Th2;
((G ** F) . s1) . a1 =
((G . s1) * (F . s1)) . a1
by MSUALG_3:2
.=
(G . s1) . ((F . s2) . a1)
by A5, A6, FUNCT_2:15
.=
((G . s2) * (F . s2)) . a1
by A5, A4, A7, FUNCT_2:15
.=
((G ** F) . s2) . a1
by MSUALG_3:2
;
hence
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
;
verum
end;
hence
G ** F is order-sorted
by Th2; verum