let A be set ; :: thesis: for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let X be non empty set ; :: thesis: for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let f be Function of X,[:(Fin A),(Fin A):]; :: thesis: for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let B be Element of Fin X; :: thesis: for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let x be Element of X; :: thesis: ( x in B implies f . x c= FinPairUnion (B,f) )
assume A1: x in B ; :: thesis: f . x c= FinPairUnion (B,f)
then (FinPairUnion A) $$ (B,f) = (FinPairUnion A) $$ ((B \/ {.x.}),f) by ZFMISC_1:40
.= (FinPairUnion A) . (((FinPairUnion A) $$ (B,f)),(f . x)) by A1, SETWISEO:20
.= ((FinPairUnion A) $$ (B,f)) \/ (f . x) by Def6 ;
hence f . x c= FinPairUnion (B,f) by Th10; :: thesis: verum