let X be functional compatible set ; :: thesis: for f being Function st f in X holds
( dom f c= dom (union X) & ( for x being set st x in dom f holds
(union X) . x = f . x ) )
let f be Function; :: thesis: ( f in X implies ( dom f c= dom (union X) & ( for x being set st x in dom f holds
(union X) . x = f . x ) ) )
assume A1: f in X ; :: thesis: ( dom f c= dom (union X) & ( for x being set st x in dom f holds
(union X) . x = f . x ) )
thus dom f c= dom (union X) :: thesis: for x being set st x in dom f holds
(union X) . x = f . x

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (union X) )
assume x in dom f ; :: thesis: x in dom (union X)
then consider y being object such that
A2: [x,y] in f by XTUPLE_0:def 12;
[x,y] in union X by A1, A2, TARSKI:def 4;
hence x in dom (union X) by XTUPLE_0:def 12; :: thesis: verum

end;

let x be set ; :: thesis: ( x in dom f implies (union X) . x = f . x )
assume x in dom f ; :: thesis: (union X) . x = f . x
then consider y being object such that
A3: [x,y] in f by XTUPLE_0:def 12;
[x,y] in union X by A1, A3, TARSKI:def 4;
hence (union X) . x = y by FUNCT_1:1
.= f . x by A3, FUNCT_1:1 ;
:: thesis: verum