set j = the Element of J;
reconsider U0 = A . the Element of J as Universal_Algebra ;
take signature U0 ; :: thesis: for j being Element of J holds signature U0 = signature (A . j)
let j1 be Element of J; :: thesis: signature U0 = signature (A . j1)
dom A = J by PARTFUN1:def 2;
hence signature U0 = signature (A . j1) by Def12; :: thesis: verum