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

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