set UF = Union F;
A1: dom J = I by PARTFUN1:def 2;
A2: dom F = I by PARTFUN1:def 2;
for x being object st x in Union F holds
ex y, z being object st x = [y,z]

proof

let x be object ; :: thesis: ( x in Union F implies ex y, z being object st x = [y,z] )
assume x in Union F ; :: thesis: ex y, z being object st x = [y,z]
then consider Y being set such that
A3: ( x in Y & Y in rng F ) by TARSKI:def 4;
consider i being object such that
A4: ( i in dom F & Y = F . i ) by A3, FUNCT_1:def 3;
reconsider i = i as Element of I by A4;
F . i is Relation ;
hence ex y, z being object st x = [y,z] by A3, A4, RELAT_1:def 1; :: thesis: verum

end;

then reconsider UF = Union F as Relation by RELAT_1:def 1;
for x, y1, y2 being object st [x,y1] in UF & [x,y2] in UF holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( [x,y1] in UF & [x,y2] in UF implies y1 = y2 )
assume A5: ( [x,y1] in UF & [x,y2] in UF ) ; :: thesis: y1 = y2
then consider Y1 being set such that
A6: ( [x,y1] in Y1 & Y1 in rng F ) by TARSKI:def 4;
consider i1 being object such that
A7: ( i1 in dom F & Y1 = F . i1 ) by A6, FUNCT_1:def 3;
reconsider i1 = i1 as Element of I by A7;
reconsider Fi1 = F . i1 as Function ;
x in dom Fi1 by A6, A7, FUNCT_1:1;
then A8: x in J . i1 by PARTFUN1:def 2;
consider Y2 being set such that
A9: ( [x,y2] in Y2 & Y2 in rng F ) by A5, TARSKI:def 4;
consider i2 being object such that
A10: ( i2 in dom F & Y2 = F . i2 ) by A9, FUNCT_1:def 3;
reconsider i2 = i2 as Element of I by A10;
reconsider Fi2 = F . i2 as Function ;
x in dom Fi2 by A9, A10, FUNCT_1:1;
then x in J . i2 by PARTFUN1:def 2;
then (J . i1) /\ (J . i2) <> {} by A8, XBOOLE_0:def 4;
then ( [x,y1] in F . i1 & [x,y2] in F . i1 ) by A6, A7, A9, A10, PROB_2:def 2, XBOOLE_0:def 7;
hence y1 = y2 by FUNCT_1:def 1; :: thesis: verum

end;

then reconsider UF = UF as Function by FUNCT_1:def 1;
A11: for x being object holds
( x in dom UF iff x in Union J )

proof

let x be object ; :: thesis: ( x in dom UF iff x in Union J )

hereby :: thesis: ( x in Union J implies x in dom UF )

assume x in dom UF ; :: thesis: x in Union J
then consider y being object such that
A12: [x,y] in UF by XTUPLE_0:def 12;
consider Y being set such that
A13: ( [x,y] in Y & Y in rng F ) by A12, TARSKI:def 4;
consider i being object such that
A14: ( i in dom F & Y = F . i ) by A13, FUNCT_1:def 3;
reconsider i = i as Element of I by A14;
reconsider Fi = F . i as Function ;
x in dom Fi by A13, A14, FUNCT_1:1;
then ( x in J . i & J . i in rng J ) by A1, FUNCT_1:3, PARTFUN1:def 2;
hence x in Union J by TARSKI:def 4; :: thesis: verum

end;

assume x in Union J ; :: thesis: x in dom UF
then consider Y being set such that
A15: ( x in Y & Y in rng J ) by TARSKI:def 4;
consider i being object such that
A16: ( i in dom J & Y = J . i ) by A15, FUNCT_1:def 3;
reconsider i = i as Element of I by A16;
reconsider Fi = F . i as Function ;
x in dom Fi by A15, A16, PARTFUN1:def 2;
then consider y being object such that
A17: [x,y] in Fi by XTUPLE_0:def 12;
Fi in rng F by A2, FUNCT_1:3;
then [x,y] in UF by A17, TARSKI:def 4;
hence x in dom UF by XTUPLE_0:def 12; :: thesis: verum

end;

for x being object st x in Union J holds
UF . x is Group

proof

let x be object ; :: thesis: ( x in Union J implies UF . x is Group )
assume x in Union J ; :: thesis: UF . x is Group
then consider Y being set such that
A18: ( x in Y & Y in rng J ) by TARSKI:def 4;
consider i being object such that
A19: ( i in dom J & Y = J . i ) by A18, FUNCT_1:def 3;
reconsider i = i as Element of I by A19;
reconsider Fi = F . i as Group-Family of J . i ;
x in dom Fi by A18, A19, PARTFUN1:def 2;
then consider y being object such that
A20: [x,y] in Fi by XTUPLE_0:def 12;
A21: y = Fi . x by A20, FUNCT_1:1;
Fi in rng F by A2, FUNCT_1:3;
then [x,y] in UF by A20, TARSKI:def 4;
then y = UF . x by FUNCT_1:1;
hence UF . x is Group by A18, A19, A21, GROUP_19:1; :: thesis: verum

end;

hence Union F is Group-Family of Union J by A11, GROUP_19:2, TARSKI:2; :: thesis: verum