let X be set ; :: thesis: for Y being non empty set
for F being FinSequence of bool [:X,Y:]
for Fy being FinSequence of bool Y
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let Y be non empty set ; :: thesis: for F being FinSequence of bool [:X,Y:]
for Fy being FinSequence of bool Y
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let F be FinSequence of bool [:X,Y:]; :: thesis: for Fy being FinSequence of bool Y
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let Fy be FinSequence of bool Y; :: thesis: for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let p be set ; :: thesis: ( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) implies X-section ((union (rng F)),p) = union (rng Fy) )
assume that
A1: dom F = dom Fy and
A2: for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ; :: thesis: X-section ((union (rng F)),p) = union (rng Fy)

now :: thesis: for q being set st q in X-section ((union (rng F)),p) holds
q in union (rng Fy)

let q be set ; :: thesis: ( q in X-section ((union (rng F)),p) implies q in union (rng Fy) )
assume q in X-section ((union (rng F)),p) ; :: thesis: q in union (rng Fy)
then consider q1 being Element of Y such that
A3: ( q = q1 & [p,q1] in union (rng F) ) ;
consider T being set such that
A4: ( [p,q1] in T & T in rng F ) by A3, TARSKI:def 4;
consider m being Element of NAT such that
A5: ( m in dom F & T = F . m ) by A4, PARTFUN1:3;
Fy . m = X-section ((F . m),p) by A1, A2, A5;
then ( q in Fy . m & Fy . m in rng Fy ) by A1, A3, A4, A5, FUNCT_1:3;
hence q in union (rng Fy) by TARSKI:def 4; :: thesis: verum

end;

then A6: X-section ((union (rng F)),p) c= union (rng Fy) ;

now :: thesis: for q being set st q in union (rng Fy) holds
q in X-section ((union (rng F)),p)

let q be set ; :: thesis: ( q in union (rng Fy) implies q in X-section ((union (rng F)),p) )
assume q in union (rng Fy) ; :: thesis: q in X-section ((union (rng F)),p)
then consider T being set such that
A7: ( q in T & T in rng Fy ) by TARSKI:def 4;
consider m being Element of NAT such that
A8: ( m in dom Fy & T = Fy . m ) by A7, PARTFUN1:3;
q in X-section ((F . m),p) by A2, A7, A8;
then consider q1 being Element of Y such that
A9: ( q = q1 & [p,q1] in F . m ) ;
F . m in rng F by A1, A8, FUNCT_1:3;
then [p,q1] in union (rng F) by A9, TARSKI:def 4;
hence q in X-section ((union (rng F)),p) by A9; :: thesis: verum

end;

then union (rng Fy) c= X-section ((union (rng F)),p) ;
hence X-section ((union (rng F)),p) = union (rng Fy) by A6; :: thesis: verum