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 st i in I holds
1_ (H . i) = 1_ G

let i be object ; :: thesis:
assume i in I ; :: thesis:
then H . i is Subgroup of G by A2;
hence 1_ (H . i) = 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;
A7: ( i in support (y,H) iff ( y . i <> 1_ (H . i) & i in I ) ) by Def1;

end;

end;