let R be non empty Poset; :: thesis: for A being OrderSortedSet of R holds id A is order-sorted
let A be OrderSortedSet of R; :: thesis: id A is order-sorted
set F = id A;
let s1, s2 be Element of R; :: according to OSALG_3:def 1 :: thesis: ( s1 <= s2 implies for a1 being set st a1 in dom ((id A) . s1) holds
( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 ) )
assume s1 <= s2 ; :: thesis: for a1 being set st a1 in dom ((id A) . s1) holds
( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 )
then A1: A . s1 c= A . s2 by OSALG_1:def 16;
let a1 be set ; :: thesis: ( a1 in dom ((id A) . s1) implies ( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 ) )
assume A2: a1 in dom ((id A) . s1) ; :: thesis: ( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 )
( A . s2 = {} implies A . s2 = {} ) ;
then dom ((id A) . s2) = A . s2 by FUNCT_2:def 1;
hence a1 in dom ((id A) . s2) by A2, A1; :: thesis: ((id A) . s1) . a1 = ((id A) . s2) . a1
((id A) . s1) . a1 = (id (A . s1)) . a1 by MSUALG_3:def 1
.= a1 by A2, FUNCT_1:18
.= (id (A . s2)) . a1 by A2, A1, FUNCT_1:18
.= ((id A) . s2) . a1 by MSUALG_3:def 1 ;
hence ((id A) . s1) . a1 = ((id A) . s2) . a1 ; :: thesis: verum