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 S1[ Element of Fin X] means ( \$1 c= B implies () \$\$ (\$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 S1[C] holds
S1[C \/ {.b.}]
let C be Element of Fin X; :: thesis: for b being Element of X st S1[C] holds
S1[C \/ {.b.}]

let b be Element of X; :: thesis: ( S1[C] implies S1[C \/ {.b.}] )
assume A3: S1[C] ; :: thesis: S1[C \/ {.b.}]
now :: thesis: ( C \/ {b} c= B implies () \$\$ ((C \/ {.b.}),f) c= c )
assume A4: C \/ {b} c= B ; :: thesis: () \$\$ ((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;
() \$\$ ((C \/ {.b.}),f) = () . ((() \$\$ (C,f)),(f . b)) by
.= (() \$\$ (C,f)) \/ (f . b) by Def6 ;
hence (FinPairUnion A) \$\$ ((C \/ {.b.}),f) c= c by ; :: thesis: verum
end;
hence S1[C \/ {.b.}] ; :: thesis: verum
end;
A6: S1[ {}. X]
proof
assume {}. X c= B ; :: thesis: () \$\$ (({}. X),f) c= c
(FinPairUnion A) \$\$ (({}. X),f) = the_unity_wrt () by ;
hence (FinPairUnion A) \$\$ (({}. X),f) c= c by Th20; :: thesis: verum
end;
for C being Element of Fin X holds S1[C] from hence FinPairUnion (B,f) c= c ; :: thesis: verum