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: ( FinPairUnion A is having_a_unity & [({}. A),({}. A)] = the_unity_wrt (FinPairUnion A) ) by Th37, Th38;
assume A2: f | B = g | B ; :: thesis: FinPairUnion B,f = FinPairUnion B,g

now

per cases ( B = {} or B <> {} ) ;

suppose A3: B = {} ; :: thesis: FinPairUnion B,f = FinPairUnion B,g

hence FinPairUnion B,f = (FinPairUnion A) $$ ({}. X),f
.= [({}. A),({}. A)] by A1, SETWISEO:40
.= (FinPairUnion A) $$ ({}. X),g by A1, SETWISEO:40
.= FinPairUnion B,g by A3 ;
:: thesis: verum

end;

suppose A4: B <> {} ; :: thesis: FinPairUnion B,f = FinPairUnion B,g

f .: B = g .: B by A2, RELAT_1:201;
hence FinPairUnion B,f = FinPairUnion B,g by A4, SETWISEO:35; :: thesis: verum

end;

end;

end;

hence FinPairUnion B,f = FinPairUnion B,g ; :: thesis: verum