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 c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
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 c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let f be Function of X,[:(Fin A),(Fin A):]; :: thesis: for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let B be Element of Fin X; :: thesis: for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let c be Element of [:(Fin A),(Fin A):]; :: thesis: ( ( for x being Element of X st x in B holds
f . x c= c ) implies FinPairUnion (B,f) c= c )
defpred S₁[ Element of Fin X] means ( $1 c= B implies (FinPairUnion A) $$ ($1,f) c= c );
assume A1: for x being Element of X st x in B holds
f . x c= c ; :: thesis: FinPairUnion (B,f) c= c

A2: now :: thesis: for C being Element of Fin X
for b being Element of X st S₁[C] holds
S₁[C \/ {.b.}]

let C be Element of Fin X; :: thesis: for b being Element of X st S₁[C] holds
S₁[C \/ {.b.}]
let b be Element of X; :: thesis: ( S₁[C] implies S₁[C \/ {.b.}] )
assume A3: S₁[C] ; :: thesis: S₁[C \/ {.b.}]

now :: thesis: ( C \/ {b} c= B implies (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c )

assume A4: C \/ {b} c= B ; :: thesis: (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c
then {b} c= B by XBOOLE_1:11;
then b in B by ZFMISC_1:31;
then A5: f . b c= c by A1;
(FinPairUnion A) $$ ((C \/ {.b.}),f) = (FinPairUnion A) . (((FinPairUnion A) $$ (C,f)),(f . b)) by Th18, SETWISEO:32
.= ((FinPairUnion A) $$ (C,f)) \/ (f . b) by Def6 ;
hence (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c by A3, A4, A5, Th9, XBOOLE_1:11; :: thesis: verum

end;

hence S₁[C \/ {.b.}] ; :: thesis: verum

end;

A6: S₁[ {}. X]

proof

assume {}. X c= B ; :: thesis: (FinPairUnion A) $$ (({}. X),f) c= c
(FinPairUnion A) $$ (({}. X),f) = the_unity_wrt (FinPairUnion A) by Th18, SETWISEO:31;
hence (FinPairUnion A) $$ (({}. X),f) c= c by Th20; :: thesis: verum

end;

for C being Element of Fin X holds S₁[C] from SETWISEO:sch 4(A6, A2);
hence FinPairUnion (B,f) c= c ; :: thesis: verum