let I be set ; :: thesis: for A being ManySortedSet of holds MSFixPoints (id A) = A
let A be ManySortedSet of ; :: thesis: MSFixPoints (id A) = A

now

let i be set ; :: thesis: ( i in I implies (MSFixPoints (id A)) . i = A . i )
assume A1: i in I ; :: thesis: (MSFixPoints (id A)) . i = A . i
thus (MSFixPoints (id A)) . i = A . i :: thesis: verum

proof

thus (MSFixPoints (id A)) . i c= A . i :: according to XBOOLE_0:def 10 :: thesis: A . i c= (MSFixPoints (id A)) . i

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (MSFixPoints (id A)) . i or x in A . i )
assume x in (MSFixPoints (id A)) . i ; :: thesis: x in A . i
then consider f being Function such that
A2: ( f = (id A) . i & x in dom f & f . x = x ) by A1, Def13;
f is Function of (A . i),(A . i) by A1, A2, PBOOLE:def 18;
hence x in A . i by A2, FUNCT_2:67; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in (MSFixPoints (id A)) . i )
assume A3: x in A . i ; :: thesis: x in (MSFixPoints (id A)) . i
reconsider f = (id A) . i as Function of (A . i),(A . i) by A1, PBOOLE:def 18;
A4: f = id (A . i) by A1, MSUALG_3:def 1;
A5: x in dom f by A3, FUNCT_2:67;
f . x = x by A3, A4, FUNCT_1:35;
hence x in (MSFixPoints (id A)) . i by A1, A5, Def13; :: thesis: verum

end;

end;

hence MSFixPoints (id A) = A by PBOOLE:3; :: thesis: verum