let I, J be non empty set ; for G being Group
for x being Function of I,G
for y being Function of J,G
for a being Function of I,J st a is onto & x = y * a holds
support y = a .: (support x)
let G be Group; for x being Function of I,G
for y being Function of J,G
for a being Function of I,J st a is onto & x = y * a holds
support y = a .: (support x)
let x be Function of I,G; for y being Function of J,G
for a being Function of I,J st a is onto & x = y * a holds
support y = a .: (support x)
let y be Function of J,G; for a being Function of I,J st a is onto & x = y * a holds
support y = a .: (support x)
let a be Function of I,J; ( a is onto & x = y * a implies support y = a .: (support x) )
assume that
A1:
a is onto
and
A2:
x = y * a
; support y = a .: (support x)
A3:
rng a = J
by A1, FUNCT_2:def 3;
then A7:
support y c= a .: (support x)
;
then
a .: (support x) c= support y
;
hence
support y = a .: (support x)
by A7, XBOOLE_0:def 10; verum