thus ( P is feasible implies for i being Element of I holds P . i in <^B,(A . i)^> ) :: thesis: ( ( for i being Element of I holds P . i in <^B,(A . i)^> ) implies P is feasible )

proof

assume A1: P is feasible ; :: thesis: for i being Element of I holds P . i in <^B,(A . i)^>
let i be Element of I; :: thesis: P . i in <^B,(A . i)^>
ex o being Object of C st
( o = A . i & P . i in <^B,o^> ) by A1;
hence P . i in <^B,(A . i)^> ; :: thesis: verum

end;

assume A2: for i being Element of I holds P . i in <^B,(A . i)^> ; :: thesis: P is feasible
let i be set ; :: according to ALTCAT_5:def 4 :: thesis: ( i in I implies ex o being Object of C st
( o = A . i & P . i in <^B,o^> ) )
assume i in I ; :: thesis: ex o being Object of C st
( o = A . i & P . i in <^B,o^> )
then reconsider i = i as Element of I ;
reconsider A = A as ObjectsFamily of I,C ;
take A . i ; :: thesis: ( A . i = A . i & P . i in <^B,(A . i)^> )
thus ( A . i = A . i & P . i in <^B,(A . i)^> ) by A2; :: thesis: verum