let R be non empty Poset; :: thesis: for A being OrderSortedSet of R
for B, C being non-empty 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; :: thesis: for B, C being non-empty 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 non-empty OrderSortedSet of R; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( a1 in A . s1 implies ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A5: a1 in A . s1 ; :: thesis: ((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 ; :: thesis: verum

end;

hence G ** F is order-sorted by Th2; :: thesis: verum