let I be set ; :: thesis: for A being ManySortedSet of I holds MSFixPoints (id A) = A
let A be ManySortedSet of I; :: thesis: MSFixPoints (id A) = A
now :: thesis: for i being object st i in I holds
(MSFixPoints (id A)) . i = A . i
let i be object ; :: 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 object ; :: 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 and
A3: x in dom f and
f . x = x by A1, Def12;
f is Function of (A . i),(A . i) by A1, A2, PBOOLE:def 15;
hence x in A . i by A3, FUNCT_2:52; :: thesis: verum
end;
reconsider f = (id A) . i as Function of (A . i),(A . i) by A1, PBOOLE:def 15;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in (MSFixPoints (id A)) . i )
assume A4: x in A . i ; :: thesis: x in (MSFixPoints (id A)) . i
A5: x in dom f by A4, FUNCT_2:52;
f = id (A . i) by A1, MSUALG_3:def 1;
then f . x = x by A4, FUNCT_1:18;
hence x in (MSFixPoints (id A)) . i by A1, A5, Def12; :: thesis: verum
end;
end;
hence MSFixPoints (id A) = A ; :: thesis: verum