let U1, U2 be Universal_Algebra; :: thesis: for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2
let S1 be Subset of U1; :: thesis: for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2
let S2 be Subset of U2; :: thesis: ( S1 = S2 implies for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2 )
assume A1: S1 = S2 ; :: thesis: for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2
let o1 be operation of U1; :: thesis: for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2
let o2 be operation of U2; :: thesis: ( o1 = o2 & S1 is_closed_on o1 implies S2 is_closed_on o2 )
assume A2: o1 = o2 ; :: thesis: ( not S1 is_closed_on o1 or S2 is_closed_on o2 )
assume A3: for s being FinSequence of S1 st len s = arity o1 holds
o1 . s in S1 ; :: according to UNIALG_2:def 3 :: thesis: S2 is_closed_on o2
let s be FinSequence of S2; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o2 or o2 . s in S2 )
reconsider s1 = s as FinSequence of S1 by A1;
assume len s = arity o2 ; :: thesis: o2 . s in S2
hence o2 . s in S2 by A1, A2, A3; :: thesis: verum