let g1, g2 be Function of (unionField (S,f,E)),L; :: thesis: ( ( for p being Element of S holds g1 | the carrier of (p `1) = p `2 ) & ( for p being Element of S holds g2 | the carrier of (p `1) = p `2 ) implies g1 = g2 )
assume AS: ( ( for p being Element of S holds g1 | the carrier of (p `1) = p `2 ) & ( for p being Element of S holds g2 | the carrier of (p `1) = p `2 ) ) ; :: thesis: g1 = g2
set K = unionField (S,f,E);
H: the carrier of (unionField (S,f,E)) = unionCarrier (S,f,E) by duf
.= union { the carrier of (p `1) where p is Element of S : verum } ;

now :: thesis: for o being object st o in the carrier of (unionField (S,f,E)) holds
g1 . o = g2 . o

let o be object ; :: thesis: ( o in the carrier of (unionField (S,f,E)) implies g1 . o = g2 . o )
assume o in the carrier of (unionField (S,f,E)) ; :: thesis: g1 . o = g2 . o
then reconsider a = o as Element of (unionField (S,f,E)) ;
consider Y1 being set such that
A1: ( a in Y1 & Y1 in { the carrier of (p `1) where p is Element of S : verum } ) by H, TARSKI:def 4;
consider p being Element of S such that
A2: Y1 = the carrier of (p `1) by A1;
reconsider a = a as Element of (p `1) by A1, A2;
g1 . a = (g1 | the carrier of (p `1)) . a by FUNCT_1:49
.= (p `2) . a by AS
.= (g2 | the carrier of (p `1)) . a by AS
.= g2 . a by FUNCT_1:49 ;
hence g1 . o = g2 . o ; :: thesis: verum

end;

hence g1 = g2 ; :: thesis: verum