let R be non empty Poset; :: thesis: 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; :: thesis: 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; :: 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

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; :: thesis: 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; :: 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

hence
G ** F is order-sorted
by Th2; :: thesis: verum
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;((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