let X be set ; for S being SigmaField of X
for N being sequence of S
for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)
let S be SigmaField of X; for N being sequence of S
for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)
let N be sequence of S; for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)
let A be Element of S; ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)
defpred S1[ object , object ] means ( $1 in NAT implies $2 = A /\ (N . $1) );
A1:
for x being object st x in NAT holds
ex y being object st
( y in S & S1[x,y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in S & S1[x,y] ) )
assume
x in NAT
;
ex y being object st
( y in S & S1[x,y] )
then reconsider x =
x as
Element of
NAT ;
consider y being
set such that A2:
y = A /\ (N . x)
;
take
y
;
( y in S & S1[x,y] )
thus
(
y in S &
S1[
x,
y] )
by A2;
verum
end;
ex F being sequence of S st
for x being object st x in NAT holds
S1[x,F . x]
from FUNCT_2:sch 1(A1);
then consider F being sequence of S such that
A3:
for x being object st x in NAT holds
S1[x,F . x]
;
take
F
; for n being Element of NAT holds F . n = A /\ (N . n)
thus
for n being Element of NAT holds F . n = A /\ (N . n)
by A3; verum