let I be set ; :: thesis:
let G be Group; :: thesis:
let H be Group-Family of I; :: thesis:
let x be Function of I,G; :: thesis:
let y be Element of (product H); :: thesis:
assume that
A1: x = y and
A2: for i being object st i in I holds
H . i is Subgroup of G ; :: thesis:
A5: for i being object
for Z being Group st i in I & Z = H . i holds
1_ Z = 1_ G

let i be object ; :: thesis:
let Z be Group; :: thesis:
assume i in I ; :: thesis:
then H . i is Subgroup of G by A2;
hence ( not Z = H . i or 1_ Z = 1_ G ) by GROUP_2:44; :: thesis:

end;

let i be object ; :: thesis:
A6: ( i in support x iff ( x . i <> 1_ G & i in I ) ) by Def2;

end;

assume A89: i in support x ; :: thesis:
then A90: ( x . i <> 1_ G & i in I ) by Def2;
reconsider Z = H . i as Group by A89, Th1;
1_ Z = 1_ G by A5, A89;
hence i in support (y,H) by A1, A90, Def1; :: thesis:

end;