let X be non empty set ; :: thesis: for A being set
for f being Function of X,(Fin A)
for B being Element of Fin X
for x being set holds
( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) )
let A be set ; :: thesis: for f being Function of X,(Fin A)
for B being Element of Fin X
for x being set holds
( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) )
let f be Function of X,(Fin A); :: thesis: for B being Element of Fin X
for x being set holds
( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) )
let B be Element of Fin X; :: thesis: for x being set holds
( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) )
let x be set ; :: thesis: ( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) )

A1: now

assume x in union (f .: B) ; :: thesis: ex i' being Element of X st
( i' in B & x in f . i' )
then consider Z being set such that
A2: x in Z and
A3: Z in f .: B by TARSKI:def 4;
f .: B is Subset of (Fin A) by Lm2;
then reconsider Z = Z as Element of Fin A by A3;
consider i being Element of X such that
A4: ( i in B & Z = f . i ) by A3, FUNCT_2:116;
take i' = i; :: thesis: ( i' in B & x in f . i' )
thus ( i' in B & x in f . i' ) by A2, A4; :: thesis: verum

end;

now

given i being Element of X such that A5: ( i in B & x in f . i ) ; :: thesis: x in union (f .: B)
f . i in f .: B by A5, FUNCT_2:43;
hence x in union (f .: B) by A5, TARSKI:def 4; :: thesis: verum

end;

hence ( x in FinUnion B,f iff ex i being Element of X st
( i in B & x in f . i ) ) by A1, Th61; :: thesis: verum