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 :: thesis: ( x in union (f .: B) implies ex i9 being Element of X st
( i9 in B & x in f . i9 ) )
assume x in union (f .: B) ; :: thesis: ex i9 being Element of X st
( i9 in B & x in f . i9 )
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:65;
take i9 = i; :: thesis: ( i9 in B & x in f . i9 )
thus ( i9 in B & x in f . i9 ) by A2, A4; :: thesis: verum
end;
now :: thesis: ( ex i being Element of X st
( i in B & x in f . i ) implies x in union (f .: B) )
given i being Element of X such that A5: i in B and
A6: x in f . i ; :: thesis: x in union (f .: B)
f . i in f .: B by A5, FUNCT_2:35;
hence x in union (f .: B) by A6, 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, Th46; :: thesis: verum