let R be non empty Poset; :: thesis: for A being OrderSortedSet of
for B, C being V5() OrderSortedSet of
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 ; :: thesis: for B, C being V5() OrderSortedSet of
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 V5() OrderSortedSet of ; :: 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 A1: ( F is order-sorted & 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 A2: s1 <= s2 ; :: thesis: for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
let a1 be set ; :: thesis: ( a1 in A . s1 implies ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A3: a1 in A . s1 ; :: thesis: ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
A4: A . s1 c= A . s2 by A2, OSALG_1:def 18;
A5: (F . s1) . a1 = (F . s2) . a1 by A1, A2, A3, Th3;
(F . s1) . a1 in B . s1 by A3, FUNCT_2:7;
then A6: (G . s1) . ((F . s2) . a1) = (G . s2) . ((F . s2) . a1) by A1, A2, A5, Th3;
((G ** F) . s1) . a1 = ((G . s1) * (F . s1)) . a1 by MSUALG_3:2
.= (G . s1) . ((F . s2) . a1) by A3, A5, FUNCT_2:21
.= ((G . s2) * (F . s2)) . a1 by A3, A4, A6, FUNCT_2:21
.= ((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 Th3; :: thesis: verum