let I be set ; :: thesis: for A, M being ManySortedSet of I
for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )

let A, M be ManySortedSet of I; :: thesis: for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )

let F be ManySortedFunction of M,M; :: thesis: ( ( A in M & F .. A = A ) iff A in MSFixPoints F )
thus ( A in M & F .. A = A implies A in MSFixPoints F ) :: thesis: ( A in MSFixPoints F implies ( A in M & F .. A = A ) )
proof
assume that
A1: A in M and
A2: F .. A = A ; :: thesis:
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in () . i )
assume A3: i in I ; :: thesis: A . i in () . i
then reconsider f = F . i as Function of (M . i),(M . i) by PBOOLE:def 15;
i in dom F by ;
then A4: f . (A . i) = A . i by ;
M = doms F by MSSUBFAM:17;
then M . i = dom f by ;
then A . i in dom f by A1, A3;
hence A . i in () . i by ; :: thesis: verum
end;
assume A5: A in MSFixPoints F ; :: thesis: ( A in M & F .. A = A )
thus A in M :: thesis: F .. A = A
proof
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in M . i )
A6: M = doms F by MSSUBFAM:17;
assume A7: i in I ; :: thesis: A . i in M . i
then A . i in () . i by A5;
then ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by ;
hence A . i in M . i by ; :: thesis: verum
end;
now :: thesis: for i being object st i in I holds
(F .. A) . i = A . i
let i be object ; :: thesis: ( i in I implies (F .. A) . i = A . i )
assume A8: i in I ; :: thesis: (F .. A) . i = A . i
then A . i in () . i by A5;
then A9: ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by ;
i in dom F by ;
hence (F .. A) . i = A . i by ; :: thesis: verum
end;
hence F .. A = A ; :: thesis: verum