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: A in MSFixPoints F
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in (MSFixPoints F) . i )
assume A3: i in I ; :: thesis: A . i in (MSFixPoints F) . i
then reconsider f = F . i as Function of (M . i),(M . i) by PBOOLE:def 15;
i in dom (F .. A) by A3, PARTFUN1:def 2;
then A4: f . (A . i) = A . i by A2, PRALG_1:def 19;
M = doms F by MSSUBFAM:17;
then M . i = dom f by A3, MSSUBFAM:14;
then A . i in dom f by A1, A3;
hence A . i in (MSFixPoints F) . i by A3, A4, Def12; :: 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 (MSFixPoints F) . i by A5;
then ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by A7, Def12;
hence A . i in M . i by A7, A6, MSSUBFAM:14; :: 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 (MSFixPoints F) . i by A5;
then A9: ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by A8, Def12;
( i in dom A & i in dom F ) by A8, PARTFUN1:def 2;
then i in (dom F) /\ (dom A) by XBOOLE_0:def 4;
then i in dom (F .. A) by PRALG_1:def 19;
hence (F .. A) . i = A . i by A9, PRALG_1:def 19; :: thesis: verum
end;
hence F .. A = A ; :: thesis: verum