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 ) )

thus A in M :: thesis: F .. A = A

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 A5:
A in MSFixPoints F
; :: thesis: ( A in M & F .. A = A )
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 by A3, PARTFUN1:def 2;

then A4: f . (A . i) = A . i by A2, PRALG_1:def 17;

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;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 by A3, PARTFUN1:def 2;

then A4: f . (A . i) = A . i by A2, PRALG_1:def 17;

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

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;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

now :: thesis: for i being object st i in I holds

(F .. A) . i = A . i

hence
F .. A = A
; :: thesis: verum(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 F by A8, PARTFUN1:def 2;

hence (F .. A) . i = A . i by A9, PRALG_1:def 17; :: thesis: verum

end;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 F by A8, PARTFUN1:def 2;

hence (F .. A) . i = A . i by A9, PRALG_1:def 17; :: thesis: verum