let S, T be non empty RelStr ; :: thesis: for f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )

A1: now :: thesis: for S, S1, T, T1 being RelStr st the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 holds
for a being Connection of S,T holds a is Connection of S1,T1
let S, S1, T, T1 be RelStr ; :: thesis: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 implies for a being Connection of S,T holds a is Connection of S1,T1 )
assume A2: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 ) ; :: thesis: for a being Connection of S,T holds a is Connection of S1,T1
let a be Connection of S,T; :: thesis: a is Connection of S1,T1
consider f being Function of S,T, g being Function of T,S such that
A3: a = [f,g] by WAYBEL_1:def 9;
reconsider g = g as Function of T1,S1 by A2;
reconsider f = f as Function of S1,T1 by A2;
a = [f,g] by A3;
hence a is Connection of S1,T1 ; :: thesis: verum
end;
( S ~ = RelStr(# the carrier of S,( the InternalRel of S ~) #) & T ~ = RelStr(# the carrier of T,( the InternalRel of T ~) #) ) ;
hence for f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) by A1; :: thesis: verum