let A be set ; :: thesis: for X being non empty set
for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)

let X be non empty set ; :: thesis: for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)

let B be Element of Fin X; :: thesis: for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)

let f, g be Function of X,[:(Fin A),(Fin A):]; :: thesis: ( f | B = g | B implies FinPairUnion (B,f) = FinPairUnion (B,g) )
set J = FinPairUnion A;
A1: [({}. A),({}. A)] = the_unity_wrt () by Th19;
assume A2: f | B = g | B ; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
now :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
per cases ( B = {} or B <> {} ) ;
suppose A3: B = {} ; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
hence FinPairUnion (B,f) = () \$\$ (({}. X),f)
.= [({}. A),({}. A)] by
.= () \$\$ (({}. X),g) by
.= FinPairUnion (B,g) by A3 ;
:: thesis: verum
end;
end;
end;
hence FinPairUnion (B,f) = FinPairUnion (B,g) ; :: thesis: verum