let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being Group-Family of J
for x being Function st a is onto holds
support (x,F) c= a .: (support ((x * a),(F * a)))
let a be Function of I,J; :: thesis: for F being Group-Family of J
for x being Function st a is onto holds
support (x,F) c= a .: (support ((x * a),(F * a)))
let F be Group-Family of J; :: thesis: for x being Function st a is onto holds
support (x,F) c= a .: (support ((x * a),(F * a)))
let x be Function; :: thesis: ( a is onto implies support (x,F) c= a .: (support ((x * a),(F * a))) )
assume A1: a is onto ; :: thesis: support (x,F) c= a .: (support ((x * a),(F * a)))
for j being object st j in support (x,F) holds
j in a .: (support ((x * a),(F * a)))

proof

let j be object ; :: thesis: ( j in support (x,F) implies j in a .: (support ((x * a),(F * a))) )
assume A2: j in support (x,F) ; :: thesis: j in a .: (support ((x * a),(F * a)))
A3: dom a = I by FUNCT_2:def 1;
rng a = J by A1, FUNCT_2:def 3;
then consider i being object such that
A4: i in I and
A5: j = a . i by A2, FUNCT_2:11;
reconsider y = x * a as Function ;
reconsider G = F * a as Group-Family of I ;
A6: 1_ (G . i) = 1_ (F . j) by A3, A4, A5, FUNCT_1:13;
x . j = y . i by A3, A4, A5, FUNCT_1:13;
then y . i <> 1_ (G . i) by A2, A6, GROUP_19:def 1;
then i in support (y,G) by A4, GROUP_19:def 1;
hence j in a .: (support ((x * a),(F * a))) by A3, A5, FUNCT_1:def 6; :: thesis: verum

end;

hence support (x,F) c= a .: (support ((x * a),(F * a))) ; :: thesis: verum