let I be set ; :: thesis: for A, X being ManySortedSet of I st A c= X holds
[|A,A|] c= [|X,X|]
let A, X be ManySortedSet of I; :: thesis: ( A c= X implies [|A,A|] c= [|X,X|] )
assume A1: A c= X ; :: thesis: [|A,A|] c= [|X,X|]
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or [|A,A|] . i c= [|X,X|] . i )
assume A2: i in I ; :: thesis: [|A,A|] . i c= [|X,X|] . i
then A . i c= X . i by A1, PBOOLE:def 5;
then [:(A . i),(A . i):] c= [:(X . i),(X . i):] by ZFMISC_1:119;
then [|A,A|] . i c= [:(X . i),(X . i):] by A2, PBOOLE:def 21;
hence [|A,A|] . i c= [|X,X|] . i by A2, PBOOLE:def 21; :: thesis: verum