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

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

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

end;

then A6: Y-section ((union (rng F)),p) c= union (rng Fx) ;

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

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

end;

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