let S be OrderSortedSign; :: thesis: for w1, w2, w3 being Element of the carrier of S * st w1 <= w2 & w2 <= w3 holds
w1 <= w3
let w1, w2, w3 be Element of the carrier of S * ; :: thesis: ( w1 <= w2 & w2 <= w3 implies w1 <= w3 )
assume that
A1: w1 <= w2 and
A2: w2 <= w3 ; :: thesis: w1 <= w3
A3: len w1 = len w2 by A1;
then A4: dom w1 = dom w2 by FINSEQ_3:29;
A5: len w2 = len w3 by A2;
then A6: dom w2 = dom w3 by FINSEQ_3:29;
for i being set st i in dom w1 holds
for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2

proof

let i be set ; :: thesis: ( i in dom w1 implies for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2 )
assume A7: i in dom w1 ; :: thesis: for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2
reconsider s3 = w1 . i, s4 = w2 . i, s5 = w3 . i as SortSymbol of S by A4, A6, A7, PARTFUN1:4;
A8: ( s3 <= s4 & s4 <= s5 ) by A1, A2, A4, A7;
let s1, s2 be SortSymbol of S; :: thesis: ( s1 = w1 . i & s2 = w3 . i implies s1 <= s2 )
assume ( s1 = w1 . i & s2 = w3 . i ) ; :: thesis: s1 <= s2
hence s1 <= s2 by A8, ORDERS_2:3; :: thesis: verum

end;

hence w1 <= w3 by A3, A5; :: thesis: verum